Charge! A framework for higher-order separation logic in Coq

DOI10.1007/978-3-642-32347-8_21MaRDI QIDQ2914751zbMATH OpenOpenAlexFDO

Authors Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal

Publication date 20 September 2012

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-32347-8_21

zbMATH Keywords

JavaCoq

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70)

Recommendations

• Verifying object-oriented programs with higher-order separation logic in Coq
• Practical Tactics for Separation Logic
• Proof tactics for assertions in separation logic
• Computer Science Logic
• Higher-order separation logic in Isabelle/HOLCF

Cited in

(11)

• \textsc{Lincx}: a linear logical framework with first-class contexts
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Modular verification of intrusive list and tree data structures in separation logic
• Temporary read-only permissions for separation logic
• A relational shape abstract domain
• Formally verifying exceptions for low-level code with separation logic
• Verifying object-oriented programs with higher-order separation logic in Coq
• Proof tactics for assertions in separation logic
• Practical Tactics for Separation Logic
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Extensible and efficient automation through reflective tactics

Describes a project that uses

Uses Software

• Charge!
• VeriFast
• Isabelle/HOL
• Coq

This page was built for publication: Charge! A framework for higher-order separation logic in Coq

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