Modular Safety Checking for Fine-Grained Concurrency
DOI10.1007/978-3-540-74061-2_15zbMATH Open1211.68082OpenAlexW1600923511MaRDI QIDQ3612005FDOQ3612005
Authors: Cristiano Calcagno, Matthew J. Parkinson, 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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (24)
- Reasoning about Separation Using Abstraction and Reification
- Concurrent Separation Logic and Operational Semantics
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Safety and Liveness in Concurrent Pointer Programs
- Concise outlines for a complex logic: a proof outline checker for TaDA
- Proving linearizability with temporal logic
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
- Balancing expressiveness in formal approaches to concurrency
- Elucidating concurrent algorithms via layers of abstraction and reification
- Automated Theorem Proving for Assertions in Separation Logic with All Connectives
- Modular inference of subprogram contracts for safety checking
- Verifying Opacity of a Transactional Mutex Lock
- Explanation of two non-blocking shared-variable communication algorithms
- Inter-process buffers in separation logic with rely-guarantee
- Mechanized proofs of opacity: a comparison of two techniques
- Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
- Title not available (Why is that?)
- Thread-modular abstraction refinement.
- Specifying and reasoning about shared-variable concurrency
- Model Checking Simulation Rules for Linearizability
- A Program Construction and Verification Tool for Separation Logic
- Caper
- A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
Uses Software
This page was built for publication: Modular Safety Checking for Fine-Grained Concurrency
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3612005)
