Authors
Simon Foster, Jonathan Julián Huerta y Munive, Georg Struth
Publication date
2020
Conference
Relational and Algebraic Methods in Computer Science: 18th International Conference, RAMiCS 2020, Palaiseau, France, October 26–29, 2020, Proceedings 18
Pages
169-186
Publisher
Springer International Publishing
Description
We present simple new Hoare logics and refinement calculi for hybrid systems in the style of differential dynamic logic. (Refinement) Kleene algebra with tests is used for reasoning about the program structure and generating verification conditions at this level. Lenses capture hybrid program stores in a generic algebraic way. The approach has been formalised with the Isabelle/HOL proof assistant. Several examples explain the workflow with the resulting verification components.
Scholar articles
S Foster, JJ Huerta y Munive, G Struth - Relational and Algebraic Methods in Computer …, 2020