Formal Techniques for Networked and Distributed Systems – FORTE 2004

DOI10.1007/b100576zbMath1110.68410OpenAlexW2244752996MaRDI QIDQ5464482

Simon Doherty, Victor Luchangco, Lindsay Groves, Mark Moir

Publication date: 18 August 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b100576

Mathematics Subject Classification ID

Related Items (12)

Model Checking Simulation Rules for Linearizability ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Making Linearizability Compositional for Partially Ordered Executions ⋮ Towards formally specifying and verifying transactional memory ⋮ Verifying correctness of persistent concurrent data structures: a sound and complete method ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Proving linearizability with temporal logic ⋮ A general technique for proving lock-freedom ⋮ Trace-based derivation of a scalable lock-free stack algorithm ⋮ Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free ⋮ Formal Verification of a Lock-Free Stack with Hazard Pointers

Uses Software

• PVS

This page was built for publication: Formal Techniques for Networked and Distributed Systems – FORTE 2004