2 papers
cs.LO2021
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs
Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher +1
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…
cs.LO2019
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
Simon Foster, Jonathan Julián Huerta y Munive, Georg Struth
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 reasonin…