1 citations · 1 across the 1 of their papers we have counts for
7 papers
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…
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…
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…