Formal Techniques for Networked and Distributed Systems – FORTE 2004

DOI10.1007/B100576zbMATH Open1110.68410OpenAlexW2244752996MaRDI QIDQ5464482FDOQ5464482

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

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

Mathematics Subject Classification ID

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

Cited In (20)

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

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)