42 citations · 206 across the 16 of their papers we have counts for
3 papers · 1 filter
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…
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL
Simon Foster, Chung-Kil Hur, Jim Woodcock
Simulation and formal verification are important complementary techniques necessary in high assurance model-based systems development. In order to support coherent results, it is n…
Certifying Differential Equation Solutions from Computer Algebra Systems in Isabelle/HOL
Thomas Hickman, Christian Pardillo Laursen, Simon Foster
The Isabelle/HOL proof assistant has a powerful library for continuous analysis, which provides the foundation for verification of hybrid systems. However, Isabelle lacks automated…