3 citations · 5 across the 3 of their papers we have counts for
10 papers
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…
Automated Verification of Reactive and Concurrent Programs by Calculation
Simon Foster, Kangfeng Ye, Ana Cavalcanti +1
Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applicati…
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…
Mechanised Assurance Cases with Integrated Formal Methods in Isabelle
Yakoub Nemouchi, Simon Foster, Mario Gleirscher +1
Assurance cases are often required as a means to certify a critical system. Use of formal methods in assurance can improve automation, and overcome problems with ambiguity, faulty…