Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification

Jonathan Julián Huerta y Munive

doi:10.1007/978-3-030-58768-0_5

Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification

Jonathan Julián Huerta y Munive^*

^*Corresponding author af dette arbejde

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

4 Citationer (Scopus)

Abstract

We formalise mathematical components for solving affine and linear systems of ordinary differential equations in Isabelle/HOL. The formalisation integrates the theory stacks of linear algebra and analysis and substantially adds content to both of them. It also serves to improve extant verification components for hybrid systems by increasing proof automation, removing certification procedures, and decreasing the number of proof obligations. We showcase these advantages through examples.

Originalsprog	Engelsk
Titel	Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings
Redaktører	Frank de Boer, Antonio Cerone
Forlag	Springer
Publikationsdato	2020
Sider	77-92
ISBN (Trykt)	9783030587673
DOI	https://doi.org/10.1007/978-3-030-58768-0_5
Status	Udgivet - 2020
Udgivet eksternt	Ja
Begivenhed	18th International Conference on Software Engineering and Formal Methods, SEFM 2020 - Amsterdam, Holland Varighed: 14 sep. 2020 → 18 sep. 2020

Konference

Konference	18th International Conference on Software Engineering and Formal Methods, SEFM 2020
Land/Område	Holland
By	Amsterdam
Periode	14/09/2020 → 18/09/2020

Navn	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind	12310 LNCS
ISSN	0302-9743

Bibliografisk note

Funding Information:
This work was funded by CONACYT?s scholarship no. 440404.. Acknowledgements. The author wishes to thank the reviewers for their insightful comments. He also thanks Georg Struth, Harsh Beohar, Rayna Dimitrova, Kirill Bogdanov and Michael Foster for discussions.

Funding Information:
This work was funded by CONACYT’s scholarship no. 440404.

Publisher Copyright:
© 2020, Springer Nature Switzerland AG.

Adgang til dokumentet

10.1007/978-3-030-58768-0_5

Andre filer og links

Link to publication in Scopus

Citationsformater

Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification. / Huerta y Munive, Jonathan Julián.
Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings. red. / Frank de Boer; Antonio Cerone. Springer, 2020. s. 77-92 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 12310 LNCS).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Huerta y Munive, JJ 2020, Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification. i F de Boer & A Cerone (red), Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 12310 LNCS, s. 77-92, 18th International Conference on Software Engineering and Formal Methods, SEFM 2020, Amsterdam, Holland, 14/09/2020. https://doi.org/10.1007/978-3-030-58768-0_5

Huerta y Munive JJ. Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification. I de Boer F, Cerone A, red., Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings. Springer. 2020. s. 77-92. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 12310 LNCS). doi: 10.1007/978-3-030-58768-0_5

Huerta y Munive, Jonathan Julián. / Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification. Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings. red. / Frank de Boer ; Antonio Cerone. Springer, 2020. s. 77-92 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 12310 LNCS).

@inproceedings{085fddf1a4e1421aada6c4475f978a88,

title = "Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification",

abstract = "We formalise mathematical components for solving affine and linear systems of ordinary differential equations in Isabelle/HOL. The formalisation integrates the theory stacks of linear algebra and analysis and substantially adds content to both of them. It also serves to improve extant verification components for hybrid systems by increasing proof automation, removing certification procedures, and decreasing the number of proof obligations. We showcase these advantages through examples.",

keywords = "Formal verification, Hybrid systems, Proof assistants",

author = "{Huerta y Munive}, {Jonathan Juli{\'a}n}",

note = "Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 18th International Conference on Software Engineering and Formal Methods, SEFM 2020 ; Conference date: 14-09-2020 Through 18-09-2020",

year = "2020",

doi = "10.1007/978-3-030-58768-0_5",

language = "English",

isbn = "9783030587673",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "77--92",

editor = "{de Boer}, Frank and Antonio Cerone",

booktitle = "Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings",

address = "Switzerland",

}

TY - GEN

T1 - Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification

AU - Huerta y Munive, Jonathan Julián

PY - 2020

Y1 - 2020

N2 - We formalise mathematical components for solving affine and linear systems of ordinary differential equations in Isabelle/HOL. The formalisation integrates the theory stacks of linear algebra and analysis and substantially adds content to both of them. It also serves to improve extant verification components for hybrid systems by increasing proof automation, removing certification procedures, and decreasing the number of proof obligations. We showcase these advantages through examples.

AB - We formalise mathematical components for solving affine and linear systems of ordinary differential equations in Isabelle/HOL. The formalisation integrates the theory stacks of linear algebra and analysis and substantially adds content to both of them. It also serves to improve extant verification components for hybrid systems by increasing proof automation, removing certification procedures, and decreasing the number of proof obligations. We showcase these advantages through examples.

KW - Formal verification

KW - Hybrid systems

KW - Proof assistants

UR - http://www.scopus.com/inward/record.url?scp=85091582650&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-58768-0_5

DO - 10.1007/978-3-030-58768-0_5

M3 - Article in proceedings

AN - SCOPUS:85091582650

SN - 9783030587673

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 77

EP - 92

BT - Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Proceedings

A2 - de Boer, Frank

A2 - Cerone, Antonio

PB - Springer

T2 - 18th International Conference on Software Engineering and Formal Methods, SEFM 2020

Y2 - 14 September 2020 through 18 September 2020

ER -