Oracle Semantics for Concurrent Separation Logic

DOI10.1007/978-3-540-78739-6_27MaRDI QIDQ5458409zbMATHOpenAlexFDO

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

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

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)

• Certifying low-level programs with hardware interrupts and preemptive threads
• Multimodal Separation Logic for Reasoning About Operational Semantics
• Barriers in Concurrent Separation Logic
• Verified software toolchain (invited talk)
• A formal C memory model for separation logic
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• A formally verified compiler back-end
• A Certified Data Race Analysis for a Java-like Language
• scientific article; zbMATH DE number 7566072 (Why is no real title available?)
• A semantics for concurrent separation logic
• A core calculus for correlation in orchestration languages
• The essence of higher-order concurrent separation logic
• A step-indexed Kripke model of hidden state
• Separation Logic for Small-Step cminor
• Revisiting concurrent separation logic
• Temporary read-only permissions for separation logic
• CONCUR 2004 - Concurrency Theory
• Concurrent separation logic and operational semantics
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• Step-indexed Kripke model of separation logic for storable locks

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)