| Correction to: Sound reasoning in tock-CSP | 0 | 0.34 | 2022 |
| Automated verification of reactive and concurrent programs by calculation | 0 | 0.34 | 2021 |
| Transforming RoboSim Models into UPPAAL | 0 | 0.34 | 2021 |
| Inputs and Outputs in CSP: A Model and a Testing Theory | 0 | 0.34 | 2020 |
| Unifying theories of reactive design contracts | 0 | 0.34 | 2020 |
| Verified simulation for robotics. | 1 | 0.41 | 2019 |
| : Specification and refinement of Safety-Critical Java programs. | 0 | 0.34 | 2019 |
| Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP. | 1 | 0.41 | 2019 |
| Probabilistic Semantics for RoboChart - A Weakest Completion Approach. | 0 | 0.34 | 2019 |
| Angelic processes for CSP via the UTP. | 0 | 0.34 | 2019 |
| Compositional and local livelock analysis for CSP. | 1 | 0.37 | 2018 |
| Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. | 1 | 0.34 | 2018 |
| Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. | 1 | 0.37 | 2018 |
| A Formal Model of the Safety-Critical Java Level 2 Paradigm. | 0 | 0.34 | 2018 |
| Modelling And Verification For Swarm Robotics | 2 | 0.37 | 2018 |
| Formalising Cosimulation Models. | 0 | 0.34 | 2017 |
| An integrated semantics for reasoning about SysML design models using refinement | 4 | 0.42 | 2017 |
| Formal mutation testing for Circus. | 3 | 0.40 | 2017 |
| Algebraic Compilation of Safety-Critical Java Bytecode. | 0 | 0.34 | 2017 |
| Avoiding useless mutants. | 0 | 0.34 | 2017 |
| Java in the Safety-Critical Domain. | 0 | 0.34 | 2016 |
| Laws of mission-based programming. | 0 | 0.34 | 2015 |
| Safety-Critical Java Virtual Machine Services | 1 | 0.36 | 2015 |
| Mobile CSP. | 0 | 0.34 | 2015 |
| Scj-Circus: A Refinement-Oriented Formal Notation For Safety-Critical Java | 0 | 0.34 | 2015 |
| NAT2TEST Tool: From Natural Language Requirements to Test Cases Based on CSP | 7 | 0.60 | 2015 |
| Assurance Cases for Block-Configurable Software | 0 | 0.34 | 2014 |
| SCJ: Memory-Safety Checking without Annotations. | 2 | 0.36 | 2014 |
| Test-data generation for control coverage by proof | 1 | 0.36 | 2014 |
| Contracts in CML. | 2 | 0.38 | 2014 |
| A Modular Theory of Object Orientation in Higher-Order UTP. | 1 | 0.37 | 2014 |
| Data Flow Coverage for Circus-Based Testing | 5 | 0.41 | 2014 |
| Refinement-based verification of implementations of Stateflow charts. | 0 | 0.34 | 2014 |
| Circus Models for Safety-Critical Java Programs. | 6 | 0.47 | 2014 |
| A Formal Model for Natural-Language Timed Requirements of Reactive Systems. | 2 | 0.39 | 2014 |
| Safety-critical Java programs from Circus models | 14 | 0.69 | 2013 |
| Refining Scj Mission Specifications Into Parallel Handler Designs | 1 | 0.35 | 2013 |
| Simulink timed models for program verification | 3 | 0.38 | 2013 |
| The Safety-Critical Java memory model formalised. | 9 | 0.55 | 2013 |
| Circus Time with Reactive Designs. | 7 | 0.56 | 2012 |
| Higher-Order UTP for a Theory of Methods. | 3 | 0.41 | 2012 |
| Mechanical reasoning about families of UTP theories | 7 | 0.54 | 2012 |
| Special issue: International Conference on Formal Engineering Methods - ICFEM 2009. | 0 | 0.34 | 2012 |
| Special issue: International Colloquium on Theoretical Aspects of Computing - ICTAC 2010 | 0 | 0.34 | 2012 |
| A tool chain for the automatic generation of circus specifications of simulink diagrams | 2 | 0.37 | 2012 |
| Features of CML: A formal modelling language for Systems of Systems | 36 | 1.55 | 2012 |
| Refinement-oriented models of Stateflow charts | 9 | 0.53 | 2012 |
| Refinement-Based Verification Of Sequential Implementations Of Stateflow Charts | 2 | 0.37 | 2011 |
| The Safety-Critical Java Mission Model: A Formal Account. | 8 | 0.49 | 2011 |
| A tactic language for refinement of state-rich concurrent specifications | 5 | 0.45 | 2011 |
