Local Reasoning for Storable Locks and Threads
From MaRDI portal
Publication:3498431
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
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