Temporal Logic Verification of Lock-Freedom

DOI10.1007/978-3-642-13321-3_21MaRDI QIDQ3575281zbMATH OpenOpenAlexFDO

Authors Bogdan Tofan, Simon Bäumler, Gerhard Schellhorn, Wolfgang Reif

Publication date 26 July 2010

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

Full work available at URL https://doi.org/10.1007/978-3-642-13321-3_21

zbMATH Keywords

verificationtemporal logiccompositional reasoninglinearizabilitylock-freedomrely-guarantee

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Specification and verification using temporal logics
• scientific article; zbMATH DE number 1487477
• Temporal Logic Verification Using Simulation
• scientific article; zbMATH DE number 2112985
• Verification of reactive systems using temporal logic with clocks
• On using temporal logic for refinement and compositional verification of concurrent systems
• Proving Failure-Free Properties of Concurrent Systems Using Temporal Logic
• scientific article; zbMATH DE number 2090286
• scientific article; zbMATH DE number 1512628
• Model-checking timed temporal logics

Cited in

(11)

• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Proving linearizability with temporal logic
• Quantitative reasoning for proving lock-freedom
• Formal verification of a lock-free stack with hazard pointers
• Towards a thread-local proof technique for starvation freedom
• Compositional reasoning using intervals and time reversal
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Proving Failure-Free Properties of Concurrent Systems Using Temporal Logic
• A sound and complete proof technique for linearizability of concurrent data structures
• Verifying Lock-Freedom Using Well-Founded Orders
• A general technique for proving lock-freedom

Describes a project that uses

Uses Software

• KIV

This page was built for publication: Temporal Logic Verification of Lock-Freedom

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