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

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)

• scientific article; zbMATH DE number 7566072 (Why is no real title available?)
• A formally verified compiler back-end
• The essence of higher-order concurrent separation logic
• A semantics for concurrent separation logic
• CONCUR 2004 - Concurrency Theory
• Multimodal Separation Logic for Reasoning About Operational Semantics
• Separation Logic for Small-Step cminor
• Concurrent separation logic and operational semantics
• Iris from the ground up: a modular foundation for 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
• Verified software toolchain (invited talk)
• A Certified Data Race Analysis for a Java-like Language
• Temporary read-only permissions for separation logic
• Step-indexed Kripke model of separation logic for storable locks
• Revisiting concurrent separation logic
• 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

Describes a project that uses

Uses Software

• cminor
• Coq

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)