| Publication | Date of Publication | Type |
|---|
Relative security: (dis)proving resilience against semantic optimization vulnerabilities in Isabelle/HOL. Extended version
Journal of Automated Reasoning | 2025-11-26 | Paper |
| Verifying correctness of persistent concurrent data structures | 2024-03-14 | Paper |
scientific article; zbMATH DE number 7774306 (Why is no real title available?)
(available as arXiv preprint) | 2023-12-08 | Paper |
Making Linearizability Compositional for Partially Ordered Executions
Lecture Notes in Computer Science | 2023-06-28 | Paper |
Making Linearizability Compositional for Partially Ordered Executions
Lecture Notes in Computer Science | 2023-06-28 | Paper |
Defining and verifying durable opacity: correctness for persistent software transactional memory
Formal Techniques for Distributed Objects, Components, and Systems | 2022-10-13 | Paper |
Modularising verification of durable opacity
(available as arXiv preprint) | 2022-08-30 | Paper |
| Modularising verification of durable opacity | 2022-08-30 | Paper |
An Observational Approach to Defining Linearizability on Weak Memory Models
Formal Techniques for Distributed Objects, Components, and Systems | 2022-06-15 | Paper |
Understanding, Explaining, and Deriving Refinement
From Astrophysics to Unconventional Computation | 2022-03-02 | Paper |
Verifying correctness of persistent concurrent data structures: a sound and complete method
Formal Aspects of Computing | 2021-09-14 | Paper |
Verifying opacity of a transactional mutex lock
FM 2015: Formal Methods | 2019-12-19 | Paper |
A framework for correctness criteria on weak memory models
FM 2015: Formal Methods | 2019-12-19 | Paper |
| Refinement | 2018-11-30 | Paper |
Mechanized proofs of opacity: a comparison of two techniques
Formal Aspects of Computing | 2018-09-12 | Paper |
| Proving opacity of a pessimistic STM | 2018-07-18 | Paper |
Model checking stochastic automata
ACM Transactions on Computational Logic | 2017-06-13 | Paper |
Relational concurrent refinement. III: Traces, partial relations and automata
Formal Aspects of Computing | 2016-08-05 | Paper |
Relational concurrent refinement: automata
Electronic Notes in Theoretical Computer Science | 2016-08-01 | Paper |
A sound and complete proof technique for linearizability of concurrent data structures
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Reasoning algebraically about refinement on TSO architectures
Theoretical Aspects of Computing – ICTAC 2014 | 2015-01-13 | Paper |
More relational concurrent refinement: traces and partial relations
Electronic Notes in Theoretical Computer Science | 2014-03-26 | Paper |
| Model checking downward simulations | 2013-12-04 | Paper |
A high-level semantics for program execution under total store order memory
Theoretical Aspects of Computing – ICTAC 2013 | 2013-10-04 | Paper |
| Unifying concurrent and relational refinement | 2013-08-19 | Paper |
Temporal-logic property preservation under Z refinement
Formal Aspects of Computing | 2013-03-22 | Paper |
| Issues in formal methods | 2012-09-05 | Paper |
| Viewpoints modelling | 2012-09-05 | Paper |
Z2SAL: a translation-based model checker for Z
Formal Aspects of Computing | 2011-05-27 | Paper |
Incompleteness of relational simulations in the blocking paradigm
Science of Computer Programming | 2010-11-25 | Paper |
Model transformations across views
Science of Computer Programming | 2010-02-26 | Paper |
Relational concurrent refinement. II: Internal operations and outputs
Formal Aspects of Computing | 2009-05-27 | Paper |
Model Transformations Incorporating Multiple Views
Algebraic Methodology and Software Technology | 2009-04-28 | Paper |
Proving Linearizability Via Non-atomic Refinement
Lecture Notes in Computer Science | 2009-03-06 | Paper |
Modelling Divergence in Relational Concurrent Refinement
Lecture Notes in Computer Science | 2009-02-24 | Paper |
On using data abstractions for model checking refinements
Acta Informatica | 2007-04-26 | Paper |
Verifying data refinements using a model checker
Formal Aspects of Computing | 2006-11-17 | Paper |
Formal program development with approximations
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Formal program development with approximations
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Non-atomic refinement in Z and CSP
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Linear temporal logic and Z refinement
Lecture Notes in Computer Science | 2005-08-25 | Paper |
Structural refinement of systems specified in Object-Z and CSP
Formal Aspects of Computing | 2005-02-08 | Paper |
Relational concurrent refinement
Formal Aspects of Computing | 2005-02-08 | Paper |
Verifying Erlang code: A resource locker case-study
Lecture Notes in Computer Science | 2004-08-12 | Paper |
Handling inconsistencies in Z using quasi-classical logic
Lecture Notes in Computer Science | 2004-08-03 | Paper |
Specification and analysis of automata-based designs
Lecture Notes in Computer Science | 2004-07-30 | Paper |
Specification and analysis of automata-based designs
Lecture Notes in Computer Science | 2004-07-30 | Paper |
Structural refinement in Object-Z / CSP
Lecture Notes in Computer Science | 2004-07-30 | Paper |
Structural refinement in Object-Z / CSP
Lecture Notes in Computer Science | 2004-07-30 | Paper |
Using coupled simulations in non-atomic refinement
Lecture Notes in Computer Science | 2003-12-04 | Paper |
Timed CSP and Object-Z
Lecture Notes in Computer Science | 2003-12-04 | Paper |
Recent advances in refinement
Lecture Notes in Computer Science | 2003-07-21 | Paper |
| Abstract specification in Object-Z and CSP | 2003-07-15 | Paper |
A UML approach to the design of open distributed systems
Lecture Notes in Computer Science | 2003-07-15 | Paper |
A formal framework for viewpoint consistency
Formal Methods in System Design | 2002-09-18 | Paper |
Combining component specifications in Object-Z and CSP.
Formal Aspects of Computing | 2002-09-09 | Paper |
Analysis of a multimedia stream using stochastic process algebra
The Computer Journal. Section A Section B | 2002-01-23 | Paper |
| scientific article; zbMATH DE number 1860618 (Why is no real title available?) | 2002-01-01 | Paper |
Specification, refinement and verification of concurrent systems -- an integration of Object-\(Z\) and \(CSP\)
Formal Methods in System Design | 2001-09-09 | Paper |
| Refinement in Z and object-Z. Foundations and advanced applications | 2001-07-10 | Paper |
Liberating data refinement
Lecture Notes in Computer Science | 2001-07-01 | Paper |
| scientific article; zbMATH DE number 1569130 (Why is no real title available?) | 2001-02-22 | Paper |
A single complete refinement rule for Z
Journal Of Logic And Computation | 2000-12-19 | Paper |
Constructive consistency checking for partial specification in Z
Science of Computer Programming | 2000-11-22 | Paper |
| Specifying component and context specification using promotion | 2000-08-10 | Paper |
| Grey box data refinement | 1999-11-02 | Paper |
| scientific article; zbMATH DE number 1304374 (Why is no real title available?) | 1999-06-17 | Paper |
Strategies for consistency checking based on unification
Science of Computer Programming | 1999-03-30 | Paper |
Specifying and refining internal operations in \(Z\)
Formal Aspects of Computing | 1999-03-09 | Paper |
| scientific article; zbMATH DE number 3412636 (Why is no real title available?) | 1967-01-01 | Paper |
