Oracle Semantics for Concurrent Separation Logic
From MaRDI portal
Publication:5458409
DOI10.1007/978-3-540-78739-6_27zbMath1133.68371OpenAlexW1584342183MaRDI QIDQ5458409
Aquinas Hobor, Andrew W. Appel, F. Zappa Nardelli
Publication date: 11 April 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-78739-6_27
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (15)
Certifying low-level programs with hardware interrupts and preemptive threads ⋮ A Certified Data Race Analysis for a Java-like Language ⋮ A formally verified compiler back-end ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ A formal C memory model for separation logic ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Temporary Read-Only Permissions for Separation Logic ⋮ The Essence of Higher-Order Concurrent Separation Logic ⋮ Verified Software Toolchain ⋮ Barriers in Concurrent Separation Logic ⋮ A step-indexed Kripke model of 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 ⋮ Unnamed Item
Uses Software
This page was built for publication: Oracle Semantics for Concurrent Separation Logic
