Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
Simon Foster, Jonathan Juli\'an Huerta y Munive, Georg Struth
TL;DR
This paper introduces new Hoare logics and refinement calculi for hybrid systems, formalized in Isabelle/HOL, enabling structured reasoning and verification of complex hybrid programs.
Contribution
It presents novel Hoare logics and refinement calculi for hybrid systems, integrating algebraic reasoning and formal verification in Isabelle/HOL.
Findings
Formalized in Isabelle/HOL
Includes examples demonstrating workflow
Enables structured reasoning about hybrid systems
Abstract
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. A number of examples explains the workflow with the resulting verification components.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.