| Publication | Date of Publication | Type |
|---|
| Weak progressive forward simulation is necessary and sufficient for strong observational refinement | 2024-08-13 | 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 |
Defining and verifying durable opacity: correctness for persistent software transactional memory
Formal Techniques for Distributed Objects, Components, and Systems | 2022-10-13 | Paper |
scientific article; zbMATH DE number 7577571 (Why is no real title available?)
(available as arXiv preprint) | 2022-08-30 | Paper |
| scientific article; zbMATH DE number 7577571 (Why is no real title available?) | 2022-08-30 | Paper |
| Flashix: modular verification of a concurrent and crash-safe flash file system | 2022-03-22 | 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 |
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 |
Towards a thread-local proof technique for starvation freedom
Lecture Notes in Computer Science | 2016-06-17 | Paper |
A sound and complete proof technique for linearizability of concurrent data structures
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Formal fault tree analysis -- practical experiences
Electronic Notes in Theoretical Computer Science | 2015-03-18 | Paper |
RGITL: a temporal logic framework for compositional reasoning about interleaved programs
Annals of Mathematics and Artificial Intelligence | 2014-07-11 | Paper |
Completeness of ASM refinement
Electronic Notes in Theoretical Computer Science | 2014-03-26 | Paper |
Formal verification of a lock-free stack with hazard pointers
Theoretical Aspects of Computing – ICTAC 2011 | 2012-01-06 | Paper |
Completeness of fair ASM refinement
Science of Computer Programming | 2011-06-06 | Paper |
Proving linearizability with temporal logic
Formal Aspects of Computing | 2011-05-27 | Paper |
Automated flaw detection in algebraic specifications
Journal of Automated Reasoning | 2011-01-12 | Paper |
Temporal Logic Verification of Lock-Freedom
Lecture Notes in Computer Science | 2010-07-26 | Paper |
Interactive verification of concurrent systems using symbolic execution
AI Communications | 2010-06-17 | Paper |
Atomic actions, and their refinements to isolated protocols
Formal Aspects of Computing | 2010-03-08 | Paper |
Relational concurrent refinement. II: Internal operations and outputs
Formal Aspects of Computing | 2009-05-27 | Paper |
Proving Linearizability Via Non-atomic Refinement
Lecture Notes in Computer Science | 2009-03-06 | Paper |
Automating Algebraic Specifications of Non-freely Generated Data Types
Automated Technology for Verification and Analysis | 2008-11-20 | Paper |
| ASM refinement preserving invariants | 2008-11-19 | Paper |
Bounded Relational Analysis of Free Data Types
Tests and Proofs | 2008-04-24 | Paper |
ASM refinement and generalizations of forward simulation in data refinement: a comparison
Theoretical Computer Science | 2005-06-10 | Paper |
Verifying Concurrent Systems with Symbolic Execution
Journal Of Logic And Computation | 2002-09-11 | Paper |
| scientific article; zbMATH DE number 1765705 (Why is no real title available?) | 2002-07-10 | Paper |
| The WAM case study: Verifying compiler correctness for Prolog with KIV | 2002-01-21 | Paper |
| Theorem proving in large theories | 2001-11-06 | Paper |
Correctness of efficient real-time model checking
Journal of Universal Computer Science | 2001-08-13 | Paper |
| scientific article; zbMATH DE number 1543041 (Why is no real title available?) | 2001-02-26 | Paper |
| scientific article; zbMATH DE number 1552508 (Why is no real title available?) | 2001-01-15 | Paper |
| scientific article; zbMATH DE number 1552511 (Why is no real title available?) | 2001-01-15 | Paper |
| scientific article; zbMATH DE number 827984 (Why is no real title available?) | 1995-12-20 | Paper |
| scientific article; zbMATH DE number 512875 (Why is no real title available?) | 1995-11-23 | Paper |
