Formal Techniques for Networked and Distributed Systems – FORTE 2004

DOI10.1007/B100576MaRDI QIDQ5464482zbMATH OpenOpenAlexFDO

Authors Simon Doherty, Lindsay Groves, Victor Luchangco, 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

Formal languages and automata (68Q45) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1500569
• Automatically verifying concurrent queue algorithms
• Temporal Logic Verification of Lock-Freedom
• Verifying concurrent data structures by simulation
• A sound and complete proof technique for linearizability of concurrent data structures

Cited in

(20)

• Nonblocking Algorithms and Backward Simulation
• An optimistic approach to lock-free FIFO queues
• Trace-based derivation of a scalable lock-free stack algorithm
• scientific article; zbMATH DE number 1500569 (Why is no real title available?)
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Model checking simulation rules for linearizability
• Making Linearizability Compositional for Partially Ordered Executions
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• Verification of Flat FIFO Systems
• Verifying correctness of persistent concurrent data structures
• Mechanized proofs of opacity: a comparison of two techniques
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Analysing lock-free linearizable datatypes using CSP
• Formal verification of a lock-free stack with hazard pointers
• Towards formally specifying and verifying transactional memory
• A general technique for proving lock-freedom
• Proving linearizability with temporal logic
• Verifying concurrent data structures by simulation
• Automatically verifying concurrent queue algorithms
• A sound and complete proof technique for linearizability of concurrent data structures

Describes a project that uses

Uses Software

• PVS

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5464482)