Local Reasoning for Storable Locks and Threads

DOI10.1007/978-3-540-76637-7_3zbMath1137.68354OpenAlexW2155032935MaRDI QIDQ3498431

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

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) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (13)

Certifying low-level programs with hardware interrupts and preemptive threads ⋮ The category-theoretic solution of recursive metric-space equations ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Temporary Read-Only Permissions for Separation Logic ⋮ Verified Software Toolchain ⋮ Barriers in Concurrent Separation Logic ⋮ Syntactic soundness proof of a type-and-capability system with hidden state ⋮ Multimodal Separation Logic for Reasoning About Operational Semantics ⋮ Step-Indexed Kripke Model of Separation Logic for Storable Locks ⋮ Concurrent Separation Logic and Operational Semantics ⋮ Verification of Concurrent Systems with VerCors ⋮ Automatic Parallelization and Optimization of Programs by Proof Rewriting ⋮ Separation Logic Contracts for a Java-Like Language with Fork/Join

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