Local Reasoning for Storable Locks and Threads

DOI10.1007/978-3-540-76637-7_3MaRDI QIDQ3498431zbMATH OpenOpenAlexFDO

Authors Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv

Publication date 15 May 2008

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-76637-7_3

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Step-indexed Kripke model of separation logic for storable locks
• CONCUR 2004 - Concurrency Theory
• A semantics for concurrent separation logic
• Programming Languages and Systems
• Fine-grained concurrency with separation logic

Cited in

(18)

• Abstract local reasoning for concurrent libraries: mind the gap
• Reasoning about lock placements
• Temporary read-only permissions for separation logic
• Verified software toolchain (invited talk)
• Barriers in Concurrent Separation Logic
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• Local linearizability for concurrent container-type data structures
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Syntactic soundness proof of a type-and-capability system with hidden state
• Verification of concurrent systems with VerCors
• Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs
• Programming Languages and Systems
• Multimodal Separation Logic for Reasoning About Operational Semantics
• Separation Logic Contracts for a Java-Like Language with Fork/Join
• Step-indexed Kripke model of separation logic for storable locks
• Concurrent separation logic and operational semantics
• The category-theoretic solution of recursive metric-space equations
• Certifying low-level programs with hardware interrupts and preemptive threads

This page was built for publication: Local Reasoning for Storable Locks and Threads

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