Modular Safety Checking for Fine-Grained Concurrency

DOI10.1007/978-3-540-74061-2_15MaRDI QIDQ3612005zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

Recommendations

• Safety and Liveness in Concurrent Pointer Programs
• scientific article; zbMATH DE number 2087551
• Thread-modular abstraction refinement.
• Expressive modular fine-grained concurrency specification
• Verification of fine-grain concurrent programs

Cited in

(28)

• Expressive modular fine-grained concurrency specification
• 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
• Proving linearizability with temporal logic
• Safety and Liveness in Concurrent Pointer Programs
• Concise outlines for a complex logic: a proof outline checker for TaDA
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Balancing expressiveness in formal approaches to concurrency
• Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
• 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
• A generalised union of rely-guarantee and separation logic using permission algebras
• 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
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• A sound and complete proof technique for linearizability of concurrent data structures
• scientific article; zbMATH DE number 522852 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

• ESC/Java
• Spec#
• Zing

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)