TY - GEN
T1 - Hybrid Systems Verification with Isabelle/HOL
T2 - 24th International Symposium on Formal Methods, FM 2021
AU - Foster, Simon
AU - Huerta y Munive, Jonathan Julián
AU - Gleirscher, Mario
AU - Struth, Georg
PY - 2021
Y1 - 2021
N2 - We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and domain-specific deductive and calculational support. The new store model yields clean separations and dynamic local views of variables, e.g. discrete/continuous, mutable/immutable, program/logical, and enhanced ways of manipulating them using combinators, projections and framing. This leads to more local inference rules, procedures and tactics for reasoning with invariant sets, certifying solutions of hybrid specifications or calculating derivatives with increased proof automation and scalability. The new expression model provides more user-friendly syntax, better control of name spaces and interfaces connecting the framework with real-world modelling languages.
AB - We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and domain-specific deductive and calculational support. The new store model yields clean separations and dynamic local views of variables, e.g. discrete/continuous, mutable/immutable, program/logical, and enhanced ways of manipulating them using combinators, projections and framing. This leads to more local inference rules, procedures and tactics for reasoning with invariant sets, certifying solutions of hybrid specifications or calculating derivatives with increased proof automation and scalability. The new expression model provides more user-friendly syntax, better control of name spaces and interfaces connecting the framework with real-world modelling languages.
U2 - 10.1007/978-3-030-90870-6_20
DO - 10.1007/978-3-030-90870-6_20
M3 - Article in proceedings
AN - SCOPUS:85119830723
SN - 9783030908690
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 367
EP - 386
BT - Formal Methods - 24th International Symposium, FM 2021, Proceedings
A2 - Huisman, Marieke
A2 - Păsăreanu, Corina
A2 - Zhan, Naijun
PB - Springer
Y2 - 20 November 2021 through 26 November 2021
ER -