Verifying object-oriented programs with higher-order separation logic in Coq

DOI10.1007/978-3-642-22863-6_5MaRDI QIDQ3087993zbMATHOpenAlexFDO

Authors Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal

Publication date 17 August 2011

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

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_5

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Charge! A framework for higher-order separation logic in Coq
• Interactive proofs in higher-order concurrent separation logic
• Effective interactive proofs for higher-order imperative programs
• Computer Science Logic
• Higher-order separation logic in Isabelle/HOLCF

Cites work

• scientific article; zbMATH DE number 944097 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• A very modal model of a modern, major, general type system
• Abstract Predicates and Mutable ADTs in Hoare Type Theory
• Frame rule for mutually recursive procedures manipulating pointers
• Higher-order separation logic in Isabelle/HOLCF
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Programming Languages and Systems
• Separation logic and abstraction
• Separation logic, abstraction and inheritance
• Step-indexed Kripke models over recursive worlds

Cited in

(13)

• Connecting higher-order separation logic to a first-order outside world
• A formal C memory model for separation logic
• Charge! A framework for higher-order separation logic in Coq
• Extensible and efficient automation through reflective tactics
• Crowfoot: A Verifier for Higher-Order Store Programs
• scientific article; zbMATH DE number 1670748 (Why is no real title available?)
• Formally verifying exceptions for low-level code with separation logic
• scientific article; zbMATH DE number 1301729 (Why is no real title available?)
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Effective interactive proofs for higher-order imperative programs
• From OBJ to ML to Coq
• On models of higher-order separation logic
• Bringing Order to the Separation Logic Jungle

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Verifying object-oriented programs with 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 Q3087993)