42 citations · 206 across the 16 of their papers we have counts for
18 papers
Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
Kangfeng Ye, Jim Woodcock, Simon Foster
Probabilistic programming combines general computer programming, statistical inference, and formal semantics to help systems make decisions when facing uncertainty. Probabilistic p…
Formally Verified Animation for RoboChart using Interaction Trees
Kangfeng Ye, Simon Foster, Jim Woodcock
RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine-based language for robotics. RoboChart supports shared var…
Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL
Simon Foster, Burkhart Wolff
Formal verification of cyber-physical and robotic systems requires that we can accurately model physical quantities that exist in the real-world. The use of explicit units in such…
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…
Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM
Simon Foster, Yakoub Nemouchi, Mario Gleirscher +2
Assurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence, and overcome errant reasoning. H…
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…
Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles
Simon Foster, Mario Gleirscher, Radu Calinescu
The use of autonomous vehicles in real-world applications is often precluded by the difficulty of providing safety guarantees for their complex controllers. The simulation-based te…
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…
Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP
Simon Foster, James Baxter, Ana Cavalcanti +2
The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and…
New Opportunities for Integrated Formal Methods
Mario Gleirscher, Simon Foster, Jim Woodcock
Formal methods have provided approaches for investigating software engineering fundamentals and also have high potential to improve current practices in dependability assurance. In…
Automating Verification of State Machines with Reactive Designs and Isabelle/UTP
Simon Foster, James Baxter, Ana Cavalcanti +2
State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal v…
Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra
Simon Foster, Kangfeng Ye, Ana Cavalcanti +1
Reactive programs are ubiquitous in modern applications, and so verification is highly desirable. We present a verification strategy for reactive programs with a large or infinite…
Unifying Theories of Reactive Design Contracts
Simon Foster, Ana Cavalcanti, Samuel Canham +2
Design-by-contract is an important technique for model-based design in which a composite system is specified by a collection of contracts that specify the behavioural assumptions a…
Towards Verification of Constituent Systems through Automated Proof
Luis Diogo Couto, Simon Foster, Richard Payne
This paper explores verification of constituent systems within the context of the Symphony tool platform for Systems of Systems (SoS). Our SoS modelling language, CML, supports var…
Dependently Typed Programming based on Automated Theorem Proving
Alasdair Armstrong, Simon Foster, Georg Struth
Mella is a minimalistic dependently typed programming language and interactive theorem prover implemented in Haskell. Its main purpose is to investigate the effective integration o…