Email Gateway (Aug 22 2022 at 20:31): Email Gateway (Aug 22 2022 at 20:31):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
the following new entry is available in the AFP.
Verification Components for Hybrid Systems
by Jonathan Julian Huerta y Munive
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.
https://www.isa-afp.org/entries/Hybrid_Systems_VCs.html
Enjoy,
René
Last updated: Apr 19 2024 at 16:20 UTC