Temporal Logic Verification of Lock-Freedom

DOI10.1007/978-3-642-13321-3_21zbMath1286.68322OpenAlexW1513633483MaRDI QIDQ3575281

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

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 logiclinearizabilitycompositional reasoninglock-freedomrely-guarantee

Mathematics Subject Classification ID

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

Related Items (4)

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Compositional reasoning using intervals and time reversal ⋮ Formal Verification of a Lock-Free Stack with Hazard Pointers

Uses Software

• KIV

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