| Publication | Date of Publication | Type |
|---|
| Formally verified animation for RoboChart using interaction trees | 2024-02-12 | Paper |
| A Survey of Practical Formal Methods for Security | 2023-08-31 | Paper |
| Automated reasoning for probabilistic sequential programs with theorem proving | 2023-03-30 | Paper |
| Learning safe neural network controllers with barrier certificates | 2022-09-01 | Paper |
| Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP | 2022-03-02 | Paper |
| Verification in the Grand Challenge | 2022-02-14 | Paper |
| Hoare and He’s Unifying Theories of Programming | 2022-02-14 | Paper |
| Editorial | 2022-01-11 | Paper |
| Non-interference through determinism | 2021-12-20 | Paper |
| RiskStructures: a design algebra for risk-aware machines | 2021-09-14 | Paper |
| Learning safe neural network controllers with barrier certificates | 2021-08-30 | Paper |
| Automated verification of reactive and concurrent programs by calculation | 2021-08-03 | Paper |
| A calculus of space, time, and causality: its algebra, geometry, logic | 2020-02-18 | Paper |
| Probabilistic semantics for RoboChart. A weakest completion approach | 2020-02-18 | Paper |
| Unifying theories of reactive design contracts | 2019-11-22 | Paper |
| Calculational verification of reactive programs with reactive relations and Kleene algebra | 2018-11-08 | Paper |
| Unifying theories of time with generalised reactive processes | 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 | 2017-04-04 | Paper |
| UTP Semantics of Reactive Processes with Continuations | 2017-04-04 | Paper |
| A Stepwise Approach to Linking Theories | 2017-04-04 | Paper |
| Obituary: Amílcar Sernadas (1952--2017) | 2017-04-03 | Paper |
| Behavioural Models for FMI Co-simulations | 2016-12-21 | Paper |
| Unifying Heterogeneous State-Spaces with Lenses | 2016-12-21 | Paper |
| Test-data generation for control coverage by proof | 2016-08-05 | Paper |
| Three Approaches to Timed External Choice in UTP | 2016-06-22 | Paper |
| Isabelle/UTP: A Mechanised Theory Engineering Framework | 2016-06-22 | Paper |
| Towards Algebraic Semantics of Circus Time | 2016-06-22 | Paper |
| CSP and Kripke Structures | 2016-02-25 | Paper |
| Using formal reasoning on a model of tasks for FreeRTOS | 2016-01-06 | Paper |
| Unifying Theories of Undefinedness in UTP | 2015-12-11 | Paper |
| Circus Time with Reactive Designs | 2015-12-11 | Paper |
| Unifying Theories of Programming in Isabelle | 2015-09-30 | Paper |
| Mechanised Wire-wise Verification of Handel-C Synthesis | 2015-03-19 | Paper |
| Unifying Theories of Logic and Specification | 2014-07-08 | Paper |
| Modelling temporal behaviour in complex systems with Timebands | 2014-06-30 | Paper |
| Safety-critical Java programs from \textsf{Circus} models | 2014-04-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2863829 | 2013-12-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2863831 | 2013-12-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2843615 | 2013-08-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2844823 | 2013-08-19 | Paper |
| Simulink Timed Models for Program Verification | 2013-08-16 | Paper |
| The safety-critical Java memory model formalised | 2013-03-22 | Paper |
| Unifying theories in ProofPower-Z | 2013-03-22 | Paper |
| Mechanised wire-wise verification of Handel-C synthesis | 2012-07-20 | Paper |
| Correct hardware synthesis | 2012-03-23 | Paper |
| The Tokeneer Experiments | 2010-10-26 | Paper |
| Unifying Theories of Interrupts | 2010-08-31 | Paper |
| UTP Semantics for Handel-C | 2010-08-31 | Paper |
| The Miracle of Reactive Programming | 2010-08-31 | Paper |
| A UTP semantics for \textsf{Circus} | 2009-05-27 | Paper |
| FDR explorer | 2009-05-27 | Paper |
| Integrated Formal Methods | 2009-05-07 | Paper |
| Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository | 2009-03-02 | Paper |
| Mechanising a formal model of flash memory | 2009-03-02 | Paper |
| POSIX file store in Z/Eves: An experiment in the verified software repository | 2009-03-02 | Paper |
| A Theory of Pointers for the UTP | 2009-01-27 | Paper |
| Proving Theorems About JML Classes | 2008-09-25 | Paper |
| Z/Eves and the Mondex Electronic Purse | 2008-09-11 | Paper |
| Unifying Theories in ProofPower-Z | 2007-09-14 | Paper |
| Pointers and Records in the Unifying Theories of Programming | 2007-09-14 | Paper |
| Mechanising a Unifying Theory | 2007-09-14 | Paper |
| Angelic nondeterminism in the unifying theories of programming | 2006-11-17 | Paper |
| The verified software repository: a step towards the verifying compiler | 2006-10-25 | Paper |
| FM 2005: Formal Methods | 2006-01-10 | Paper |
| Mathematics of Program Construction | 2005-08-26 | Paper |
| ArcAngel: a tactic language for refinement | 2005-02-08 | Paper |
| A refinement strategy for Circus | 2005-02-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4808845 | 2004-08-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4472182 | 2004-08-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4412473 | 2003-07-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4494250 | 2000-08-10 | Paper |
| An inconsistency in procedures, parameters, and substitution in the refinement calculus | 2000-01-04 | Paper |
| ZRC -- A refinement calculus for \(Z\) | 1999-06-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4250672 | 1999-06-17 | Paper |
| A Weakest Precondition Semantics for Z | 1998-08-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4370267 | 1998-04-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4301167 | 1994-07-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3364231 | 1994-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3992808 | 1993-01-23 | Paper |
| Transaction processing primitives and CSP | 1987-01-01 | Paper |
