Oracle Semantics for Concurrent Separation Logic

DOI10.1007/978-3-540-78739-6_27MaRDI QIDQ5458409zbMATH OpenOpenAlexFDO

Authors 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

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• CONCUR 2004 - Concurrency Theory
• A semantics for concurrent separation logic
• Separation Logic for Small-Step cminor
• Concurrent separation logic and operational semantics
• Revisiting concurrent separation logic

Cited in

(20)

• A formal C memory model for separation logic
• Revisiting concurrent separation logic
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• A formally verified compiler back-end
• Temporary read-only permissions for separation logic
• The essence of higher-order concurrent separation logic
• Verified software toolchain (invited talk)
• Barriers in Concurrent Separation Logic
• A Certified Data Race Analysis for a Java-like Language
• Separation Logic for Small-Step cminor
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• A step-indexed Kripke model of hidden state
• \textbf{Actris 2.0}: asynchronous session-type based reasoning in separation logic
• CONCUR 2004 - Concurrency Theory
• Multimodal Separation Logic for Reasoning About Operational Semantics
• Step-indexed Kripke model of separation logic for storable locks
• Concurrent separation logic and operational semantics
• Certifying low-level programs with hardware interrupts and preemptive threads
• A core calculus for correlation in orchestration languages
• A semantics for concurrent separation logic

Describes a project that uses

Uses Software

• Coq
• cminor

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)