Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq

DOI10.1007/978-3-642-22863-6_5zbMath1342.68203OpenAlexW1848615987MaRDI QIDQ3087993

Filip Sieczkowski, Jonas Braband Jensen, Jesper Bengtson, 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

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

Related Items (5)

On models of higher-order separation logic ⋮ Bringing Order to the Separation Logic Jungle ⋮ Formally verifying exceptions for low-level code with separation logic ⋮ A formal C memory model for separation logic ⋮ Extensible and Efficient Automation Through Reflective Tactics

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Frame rule for mutually recursive procedures manipulating pointers
• A very modal model of a modern, major, general type system
• Separation logic, abstraction and inheritance
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Separation logic and abstraction
• Programming Languages and Systems
• Step-indexed kripke models over recursive worlds
• Higher-Order Separation Logic in Isabelle/HOLCF
• Abstract Predicates and Mutable ADTs in Hoare Type Theory

This page was built for publication: Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq