Abstract
These components formalise a semantic framework for the deductive
verification of hybrid systems. They support reasoning about
continuous evolutions of hybrid programs in the style of differential
dynamics logic. Vector fields or flows model these evolutions, and
their verification is done with invariants for the former or orbits
for the latter. Laws of modal Kleene algebra or categorical predicate
transformers implement the verification condition generation. Examples
show the approach at work.
License
History
- December 13, 2020
- added components based on Kleene algebras with tests. These implement differential Hoare logic (dH) and a Morgan-style differential refinement calculus (dR) for verification of hybrid programs.