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 (27)
- Automated theorem proving for assertions in separation logic with all connectives
- 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
- Concurrent separation logic and operational semantics
- Reasoning about separation using abstraction and reification
- Model checking simulation rules for linearizability
- Modular inference of subprogram contracts for safety checking
- Explanation of two non-blocking shared-variable communication algorithms
- Inter-process buffers in separation logic with rely-guarantee
- Dynamically checking ownership policies in concurrent C/C++ programs
- 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
- 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?)
- Verifying opacity of a transactional mutex lock
- Thread-modular abstraction refinement.
- Specifying and reasoning about shared-variable concurrency
- Caper
- Extracting safe thread schedules from incomplete model checking results
- Expressive modular fine-grained concurrency specification
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)
