Certificates and Separation Logic

DOI10.1007/978-3-319-05119-2_16MaRDI QIDQ2830040zbMATH OpenOpenAlexFDO

Authors Martin Nordio, Cristiano Calcagno, Bertrand Meyer

Publication date 9 November 2016

Published in Trustworthy Global Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-05119-2_16

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Separation logic and abstraction
• Separation logic and concurrency
• Verifiable certificates for predicate subtyping
• A Marriage of Rely/Guarantee and Separation Logic
• Independence and concurrent separation logic
• Foundational proof certificates in first-order logic
• Practical Tactics for Separation Logic
• Proof tactics for assertions in separation logic
• Certification Using the Mobius Base Logic

Cites work

• Enhancing modular OO verification with separation logic
• Preservation of Proof Obligations from Java to the Java Virtual Machine
• Program and proof optimizations with type systems
• Programming Languages and Systems
• Resources, concurrency, and local reasoning
• Separation and information hiding
• Separation logic, abstraction and inheritance

Cited in

(3)

• Lightweight verification of separate compilation
• An Introduction to Certificate Translation
• Preservation of Proof Obligations from Java to the Java Virtual Machine

Describes a project that uses

Uses Software

• jStar

This page was built for publication: Certificates and Separation Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2830040)