Formal Techniques for Networked and Distributed Systems – FORTE 2004
From MaRDI portal
Publication:5464482
DOI10.1007/b100576zbMath1110.68410MaRDI 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
68Q45: Formal languages and automata
68Q60: Specification and verification (program logics, model checking, etc.)
68P05: Data structures
Related Items
Model Checking Simulation Rules for Linearizability, Making Linearizability Compositional for Partially Ordered Executions, Towards formally specifying and verifying transactional memory, Proving linearizability with temporal logic, A general technique for proving lock-freedom, Trace-based derivation of a scalable lock-free stack algorithm, Mechanized proofs of opacity: a comparison of two techniques, Verifying correctness of persistent concurrent data structures: a sound and complete method, Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free, RGITL: a temporal logic framework for compositional reasoning about interleaved programs, A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures, Formal Verification of a Lock-Free Stack with Hazard Pointers
Uses Software