2 citations · 2 across the 3 of their papers we have counts for
4 papers · 1 filter
Scenes: A Meta-Logical Algebra for Mutable State
Simon Foster, Carlos Isasa, Christian Pardillo Laursen
Modelling of mutable state spaces and precisely describing how variables are manipulated in a program is a fundamental problem in compositional verification. Though we can make use…
Brownian Motion in Isabelle/HOL
Christian Pardillo Laursen, Simon Foster, Mark Post
In order to formally verify robotic controllers, we must tackle the inherent uncertainty of sensing and actuation in a physical environment. We can model uncertainty using stochast…
Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
Jonathan Julián Huerta y Munive, Simon Foster, Mario Gleirscher +3
We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic fo…
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…