An integrated specification and verification technique for highly concurrent data structures

DOI10.1007/978-3-642-36742-7_23MaRDI QIDQ5326334zbMATH OpenOpenAlexFDO

Authors Frédéric Haziza, Lukáš Holik, Ahmed Rezine, Parosh A. Abdulla, Bengt Jonsson

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

Data structures (68P05) 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)

Recommendations

• Verifying concurrent data structures by simulation
• Fragment abstraction for concurrent shape analysis
• Automatically verifying concurrent queue algorithms
• scientific article; zbMATH DE number 1948389
• A sound and complete proof technique for linearizability of concurrent data structures

Cited in

(27)

• An abstraction technique for describing concurrent program behaviour
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Highly dependable concurrent programming using design for verification
• Formalization and correctness of a concurrent linear hash structure algorithm using nested transactions and I/O automata
• Resource protection using atomics. Patterns and verification
• Automatically verifying concurrent queue algorithms
• Interface-based specification and verification of concurrency controllers
• Verifying concurrent data structures by simulation
• Decomposable relaxation for concurrent data structures
• Abstract specifications for concurrent maps
• Verification of heap manipulating programs with ordered data by extended forest automata
• Formal verification of a lock-free stack with hazard pointers
• Verification of higher-order concurrent programs with dynamic resource creation
• Safety and Liveness in Concurrent Pointer Programs
• scientific article; zbMATH DE number 4041239 (Why is no real title available?)
• scientific article; zbMATH DE number 1948389 (Why is no real title available?)
• scientific article; zbMATH DE number 1487480 (Why is no real title available?)
• Verifying visibility-based weak consistency
• Order out of chaos: proving linearizability using local views
• Concurrent program verification with invariant-guided underapproximation
• Checking linearizability of concurrent priority queues
• Verifying safety properties of concurrent Java programs using 3-valued logic
• View abstraction -- a tutorial (invited paper)
• Expressive modular fine-grained concurrency specification
• Verifying correctness of persistent concurrent data structures
• Practical abstractions for automated verification of shared-memory concurrency

This page was built for publication: An integrated specification and verification technique for highly concurrent data structures

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