An Integrated Specification and Verification Technique for Highly Concurrent Data Structures

DOI10.1007/978-3-642-36742-7_23zbMath1381.68141OpenAlexW1511438294MaRDI QIDQ5326334

Frédéric Haziza, Ahmed Rezine, Lukáš Holík, Bengt Jonsson, Parosh Aziz Abdulla

Publication date: 5 August 2013

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-36742-7_23

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Data structures (68P05)

Related Items (8)

Verifying Visibility-Based Weak Consistency ⋮ Verification of heap manipulating programs with ordered data by extended forest automata ⋮ On reducing linearizability to state reachability ⋮ Unnamed Item ⋮ Decomposable Relaxation for Concurrent Data Structures ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free

This page was built for publication: An Integrated Specification and Verification Technique for Highly Concurrent Data Structures