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

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) 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)

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

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)