research
∙
03/16/2023
Probabilistic relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
Probabilistic programming combines general computer programming, statist...
share
research
∙
03/16/2023
Formally Verified Animation for RoboChart using Interaction Trees
RoboChart is a core notation in the RoboStar framework. It is a timed an...
research
∙
02/15/2023
Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL
Formal verification of cyber-physical and robotic systems requires that ...
research
∙
06/10/2021
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs
We extend a semantic verification framework for hybrid systems with the ...
research
∙
05/11/2021
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL
Simulation and formal verification are important complementary technique...
research
∙
02/04/2021
Certifying Differential Equation Solutions from Computer Algebra Systems in Isabelle/HOL
The Isabelle/HOL proof assistant has a powerful library for continuous a...
research
∙
09/25/2020
Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM
Assurance cases are often required to certify critical systems. The use ...
research
∙
07/27/2020
Automated Verification of Reactive and Concurrent Programs by Calculation
Reactive programs combine traditional sequential programming constructs ...
research
∙
06/16/2020
Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles
The use of autonomous vehicles in real-world applications is often precl...
research
∙
10/29/2019
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
We present simple new Hoare logics and refinement calculi for hybrid sys...
research
∙
05/15/2019
Mechanised Assurance Cases with Integrated Formal Methods in Isabelle
Assurance cases are often required as a means to certify a critical syst...
research
∙
05/14/2019
Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP
The growing complexity and diversity of models used in the engineering o...
research
∙
12/25/2018
New Opportunities for Integrated Formal Methods
Formal methods have provided approaches for investigating software engin...
research
∙
12/25/2018
Assuring Autonomous Systems: Opportunities for Integrated Formal Methods?
Formal methods have provided approaches for investigating software engin...
research
∙
07/23/2018
Automating Verification of State Machines with Reactive Designs and Isabelle/UTP
State-machine based notations are ubiquitous in the description of compo...
research
∙
06/06/2018
Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra
Reactive programs are ubiquitous in modern applications, and thus verifi...
research
∙
12/29/2017
Unifying Theories of Reactive Design Contracts
Design-by-contract is an important technique for model-based design in w...
research
∙
12/29/2017
Unifying Theories of Time with Generalised Reactive Processes
Hoare and He's theory of reactive processes provides a unifying foundati...
research
∙
12/29/2017