Oracle Semantics for Concurrent Separation Logic
From MaRDI portal
Publication:5458409
DOI10.1007/978-3-540-78739-6_27zbMATH Open1133.68371OpenAlexW1584342183MaRDI QIDQ5458409FDOQ5458409
Aquinas Hobor, Andrew W. Appel, Francesco 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
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)
Cited In (19)
- Concurrent Separation Logic and Operational Semantics
- Title not available (Why is that?)
- A formally verified compiler back-end
- A semantics for concurrent separation logic
- CONCUR 2004 - Concurrency Theory
- Multimodal Separation Logic for Reasoning About Operational Semantics
- Separation Logic for Small-Step cminor
- Step-Indexed Kripke Model of Separation Logic for Storable Locks
- The Essence of Higher-Order Concurrent Separation Logic
- Barriers in Concurrent Separation Logic
- A core calculus for correlation in orchestration languages
- Certifying low-level programs with hardware interrupts and preemptive threads
- A Certified Data Race Analysis for a Java-like Language
- A step-indexed Kripke model of hidden state
- 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
- Verified Software Toolchain
- Temporary Read-Only Permissions for Separation Logic
Uses Software
This page was built for publication: Oracle Semantics for Concurrent Separation Logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458409)
