| Publication | Date of Publication | Type |
|---|
IsaVODEs: Interactive verification of cyber-physical systems at scale
Journal of Automated Reasoning | 2024-12-16 | Paper |
Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
Theoretical Computer Science | 2024-11-18 | Paper |
| Evolution of Formal Model-Based Assurance Cases for Autonomous Robots | 2024-03-14 | Paper |
| UTP, \textsf{\textit{Circus}}, and Isabelle | 2024-02-28 | Paper |
Formally verified animation for RoboChart using interaction trees
Journal of Logical and Algebraic Methods in Programming | 2024-02-12 | Paper |
| Automated reasoning for probabilistic sequential programs with theorem proving | 2023-03-30 | Paper |
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
Relational and Algebraic Methods in Computer Science | 2022-08-30 | Paper |
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
Relational and Algebraic Methods in Computer Science | 2022-08-30 | Paper |
Automated Algebraic Reasoning for Collections and Local Variables with Lenses
Relational and Algebraic Methods in Computer Science | 2022-08-30 | Paper |
Compositional assume-guarantee reasoning of control law diagrams using UTP
From Astrophysics to Unconventional Computation | 2022-03-02 | Paper |
Verification in the Grand Challenge
Theories of Programming | 2022-02-14 | Paper |
Integration of formal proof into unified assurance cases with Isabelle/SACM
Formal Aspects of Computing | 2022-01-11 | Paper |
Automated verification of reactive and concurrent programs by calculation
Journal of Logical and Algebraic Methods in Programming | 2021-08-03 | Paper |
| Hybrid relations in Isabelle/UTP | 2020-02-18 | Paper |
| Probabilistic semantics for RoboChart. A weakest completion approach | 2020-02-18 | Paper |
Unifying theories of reactive design contracts
Theoretical Computer Science | 2019-11-22 | Paper |
Unifying theories of reactive design contracts
Theoretical Computer Science | 2019-11-22 | Paper |
Calculational verification of reactive programs with reactive relations and Kleene algebra
(available as arXiv preprint) | 2018-11-08 | Paper |
| Calculational verification of reactive programs with reactive relations and Kleene algebra | 2018-11-08 | Paper |
Unifying theories of time with generalised reactive processes
Information Processing Letters | 2018-04-05 | Paper |
Unifying theories of time with generalised reactive processes
Information Processing Letters | 2018-04-05 | Paper |
| Towards verification of cyber-physical systems with UTP and Isabelle/HOL | 2018-03-26 | Paper |
Towards a UTP semantics for Modelica
Unifying Theories of Programming | 2017-04-04 | Paper |
An Axiomatic Value Model for Isabelle/UTP
Unifying Theories of Programming | 2017-04-04 | Paper |
Unifying heterogeneous state-spaces with lenses
Theoretical Aspects of Computing – ICTAC 2016 | 2016-12-21 | Paper |
Isabelle/UTP: a mechanised theory engineering framework
Unifying Theories of Programming | 2016-06-22 | Paper |
Unifying theories of programming in Isabelle
Lecture Notes in Computer Science | 2015-09-30 | Paper |
On the fine-structure of regular algebra
Journal of Automated Reasoning | 2015-07-02 | Paper |
Automated analysis of regular algebra
Automated Reasoning | 2012-09-05 | Paper |
Dependently Typed Programming Based on Automated Theorem Proving
Lecture Notes in Computer Science | 2012-09-05 | Paper |
Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
Relational and Algebraic Methods in Computer Science | 2011-06-17 | Paper |
