| Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement | 0 | 0.34 | 2022 |
| Brief Announcement - On Strong Observational Refinement and Forward Simulation. | 0 | 0.34 | 2021 |
| Verifying correctness of persistent concurrent data structures: a sound and complete method | 0 | 0.34 | 2021 |
| Flashix - Modular Verification of a Concurrent and Crash-Safe Flash File System. | 0 | 0.34 | 2021 |
| Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory | 0 | 0.34 | 2020 |
| Adding Concurrency to a Sequential Refinement Tower. | 0 | 0.34 | 2020 |
| Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch. | 0 | 0.34 | 2020 |
| Verifying Correctness of Persistent Concurrent Data Structures. | 0 | 0.34 | 2019 |
| Mechanized proofs of opacity: a comparison of two techniques. | 1 | 0.36 | 2018 |
| FastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity. | 0 | 0.34 | 2018 |
| Symbolic execution for a clash-free subset of ASMs. | 1 | 0.36 | 2018 |
| Modular Verification of Order-Preserving Write-Back Caches. | 1 | 0.35 | 2017 |
| A Relational Encoding for a Clash-Free Subset of ASMs. | 1 | 0.36 | 2016 |
| Proving Opacity of a Pessimistic STM. | 0 | 0.34 | 2016 |
| Modular, crash-safe refinement for ASMs with submachines. | 2 | 0.37 | 2016 |
| Towards a Thread-Local Proof Technique for Starvation Freedom. | 0 | 0.34 | 2016 |
| KIV: overview and VerifyThis competition. | 16 | 0.74 | 2015 |
| Inside a Verified Flash File System: Transactions and Garbage Collection. | 6 | 0.44 | 2015 |
| Verifying opacity of a transactional Mutex lock | 7 | 0.56 | 2015 |
| Verification of B$$^+$$ trees by integration of shape analysis and interactive theorem proving | 0 | 0.34 | 2015 |
| Two approaches for proving linearizability of multiset. | 1 | 0.35 | 2014 |
| Modular Refinement for Submachines of ASMs. | 4 | 0.41 | 2014 |
| Quiescent Consistency: Defining and Verifying Relaxed Linearizability. | 8 | 0.44 | 2014 |
| Development of a Verified Flash File System. | 12 | 0.56 | 2014 |
| A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures | 23 | 0.82 | 2014 |
| RGITL: A temporal logic framework for compositional reasoning about interleaved programs | 10 | 0.61 | 2014 |
| Formal Specification of an Erase Block Management Layer for Flash Memory. | 5 | 0.44 | 2013 |
| Verification of a Virtual Filesystem Switch. | 15 | 0.71 | 2013 |
| Compositional Verification of a Lock-Free Stack with RGITL. | 2 | 0.37 | 2013 |
| How to prove algorithms linearisable | 23 | 0.81 | 2012 |
| A Formal Model Of A Virtual Filesystem Switch | 7 | 0.57 | 2012 |
| Proving Linearizability of Multiset with Local Proof Obligations. | 3 | 0.37 | 2012 |
| Formal verification of a lock-free stack with hazard pointers | 11 | 0.59 | 2011 |
| Verifying linearisability with potential linearisation points | 22 | 0.94 | 2011 |
| The COST IC0701 verification competition 2011 | 12 | 0.58 | 2011 |
| Completeness of fair ASM refinement | 10 | 0.51 | 2011 |
| Selected papers of the Refinement Workshop Turku (2008) | 0 | 0.34 | 2011 |
| Proving linearizability with temporal logic | 16 | 0.71 | 2011 |
| Mondex: Engineering a Provable Secure Electronic Purse. | 2 | 0.37 | 2011 |
| Mechanically verified proof obligations for linearizability | 28 | 0.98 | 2011 |
| Extending ITL with Interleaved Programs for Interactive Verification | 0 | 0.34 | 2011 |
| Interleaved Programs and Rely-Guarantee Reasoning with ITL | 16 | 0.72 | 2011 |
| Simulating a Flash File System with CoreASM and Eclipse. | 0 | 0.34 | 2011 |
| Automated Flaw Detection in Algebraic Specifications | 3 | 0.40 | 2010 |
| Interactive verification of concurrent systems using symbolic execution | 17 | 0.76 | 2010 |
| Temporal logic verification of lock-freedom | 10 | 0.56 | 2010 |
| Atomic actions, and their refinements to isolated protocols | 7 | 0.47 | 2010 |
| Relational concurrent refinement part II: Internal operations and outputs | 13 | 0.59 | 2009 |
| Abstract Specification of the UBIFS File System for Flash Memory | 19 | 1.15 | 2009 |
| Formal Verification of Lock-Free Algorithms | 0 | 0.34 | 2009 |
