Verifying object-oriented programs with higher-order separation logic in Coq
DOI10.1007/978-3-642-22863-6_5zbMATH Open1342.68203OpenAlexW1848615987MaRDI QIDQ3087993FDOQ3087993
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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Nested Hoare Triples and Frame Rules for Higher-Order Store
- Programming Languages and Systems
- Step-indexed kripke models over recursive worlds
- Title not available (Why is that?)
- Separation logic and abstraction
- A very modal model of a modern, major, general type system
- Separation logic, abstraction and inheritance
- Frame rule for mutually recursive procedures manipulating pointers
- Abstract Predicates and Mutable ADTs in Hoare Type Theory
- Higher-Order Separation Logic in Isabelle/HOLCF
Cited In (11)
- On models of higher-order separation logic
- Extensible and Efficient Automation Through Reflective Tactics
- Bringing Order to the Separation Logic Jungle
- Extending Coq with Imperative Features and Its Application to SAT Verification
- Charge! A framework for higher-order separation logic in Coq
- Title not available (Why is that?)
- Formally verifying exceptions for low-level code with separation logic
- From OBJ to ML to Coq
- A formal C memory model for separation logic
- Title not available (Why is that?)
- Crowfoot: A Verifier for Higher-Order Store Programs
Uses Software
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)
