Modular Safety Checking for Fine-Grained Concurrency

DOI10.1007/978-3-540-74061-2_15zbMath1211.68082OpenAlexW1600923511MaRDI QIDQ3612005

Matthew J. Parkinson, Cristiano Calcagno, Viktor Vafeiadis

Publication date: 3 March 2009

Published in: Static Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74061-2_15

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (19)

Caper ⋮ Automated Theorem Proving for Assertions in Separation Logic with All Connectives ⋮ Model Checking Simulation Rules for Linearizability ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ A Program Construction and Verification Tool for Separation Logic ⋮ A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Inter-process buffers in separation logic with rely-guarantee ⋮ Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification ⋮ Explanation of two non-blocking shared-variable communication algorithms ⋮ Proving linearizability with temporal logic ⋮ Elucidating concurrent algorithms via layers of abstraction and reification ⋮ Concurrent Separation Logic and Operational Semantics ⋮ Verifying Opacity of a Transactional Mutex Lock ⋮ Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free ⋮ On the relation between concurrent separation logic and concurrent Kleene algebra ⋮ Reasoning about Separation Using Abstraction and Reification

Uses Software

• Zing
• Spec#
• ESC/Java

This page was built for publication: Modular Safety Checking for Fine-Grained Concurrency