Verifying Lock-Freedom Using Well-Founded Orders

DOI10.1007/978-3-540-75292-9_9MaRDI QIDQ3525079zbMATH OpenOpenAlexFDO

Authors Robert Colvin, Brijesh Dongol

Publication date 17 September 2008

Published in Theoretical Aspects of Computing – ICTAC 2007 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75292-9_9

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• A general technique for proving lock-freedom
• Temporal Logic Verification of Lock-Freedom
• Formal verification of a lock-free stack with hazard pointers
• Computer Aided Verification

Cited in

(3)

• Quantitative reasoning for proving lock-freedom
• Formal verification of a lock-free stack with hazard pointers
• A general technique for proving lock-freedom

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Verifying Lock-Freedom Using Well-Founded Orders

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