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