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

DOI10.1007/978-3-642-32347-8_21zbMATH Open1360.68741OpenAlexW4236538466MaRDI QIDQ2914751FDOQ2914751

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

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

zbMATH Keywords

JavaCoq

Mathematics Subject Classification ID

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

Cited In (10)

• \textsc{Lincx}: a linear logical framework with first-class contexts
• Iris from the ground up: a modular foundation for higher-order concurrent 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
• Practical Tactics for Separation Logic
• Proof tactics for assertions in separation logic
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Extensible and efficient automation through reflective tactics

Uses Software

• Coq
• Isabelle/HOL
• VeriFast
• Charge!

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)