Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs

Simon David Foster; Jonathan Huerta y Munive; Georg Struth; Mario Gleirscher

doi:10.1007/978-3-030-90870-6_20

Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs

Simon David Foster, Jonathan Huerta y Munive, Georg Struth, Mario Gleirscher

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	Formal methods
Subtitle of host publication	24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings
Publisher	Springer
Pages	367-386
Number of pages	18
ISBN (Electronic)	978-3-030-90870-6
ISBN (Print)	978-3-030-90869-0
DOIs	https://doi.org/10.1007/978-3-030-90870-6_20
Publication status	Published - 10 Nov 2021

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13047

Access to Document

10.1007/978-3-030-90870-6_20

https://arxiv.org/abs/2106.05987

Cite this

Foster, S. D., Munive, J. H. Y., Struth, G., & Gleirscher, M. (2021). Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. In Formal methods: 24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings (pp. 367-386). (Lecture Notes in Computer Science; Vol. 13047). Springer. https://doi.org/10.1007/978-3-030-90870-6_20

@inproceedings{77df7349c8384da5bf130c7549fdca79,

title = "Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs",

abstract = "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.",

author = "Foster, {Simon David} and Munive, {Jonathan Huerta y} and Georg Struth and Mario Gleirscher",

year = "2021",

month = nov,

day = "10",

doi = "10.1007/978-3-030-90870-6_20",

language = "English",

isbn = "978-3-030-90869-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "367--386",

booktitle = "Formal methods",

address = "Germany",

}

Foster, SD, Munive, JHY, Struth, G & Gleirscher, M 2021, Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. in Formal methods: 24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings. Lecture Notes in Computer Science, vol. 13047, Springer, pp. 367-386. https://doi.org/10.1007/978-3-030-90870-6_20

Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. / Foster, Simon David; Munive, Jonathan Huerta y; Struth, Georg et al.
Formal methods: 24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings. Springer, 2021. p. 367-386 (Lecture Notes in Computer Science; Vol. 13047).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Hybrid Systems Verification with Isabelle/HOL

T2 - Simpler Syntax, Better Models, Faster Proofs

AU - Foster, Simon David

AU - Munive, Jonathan Huerta y

AU - Struth, Georg

AU - Gleirscher, Mario

PY - 2021/11/10

Y1 - 2021/11/10

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 - Conference contribution

SN - 978-3-030-90869-0

T3 - Lecture Notes in Computer Science

SP - 367

EP - 386

BT - Formal methods

PB - Springer

ER -