Crowfoot: A Verifier for Higher-Order Store Programs

DOI10.1007/978-3-642-27940-9_10MaRDI QIDQ2891407zbMATH OpenOpenAlexFDO

Authors Nathaniel Charlton, Ben Horsfall, Bernhard Reus

Publication date 15 June 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://sro.sussex.ac.uk/id/eprint/31151/1/REUS_crowfoot.pdf

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

• Symbolic execution proofs for higher order store programs
• A verified proof checker for higher-order logic
• The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification
• Verifying object-oriented programs with higher-order separation logic in Coq
• Higher-order program verification via HFL model checking
• Types and higher-order recursion schemes for verification of higher-order programs

Cites work

• A semantic foundation for hidden state
• An observationally complete program logic for imperative higher-order functions
• Automated Verification of Shape and Size Properties Via Separation Logic
• Certified assembly programming with embedded code pointers
• Hoare type theory, polymorphism and separation
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Programming Languages and Systems
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Specification patterns and proofs for recursion through the store

Cited in

(2)

• Specification patterns for reasoning about recursion through the store
• Symbolic execution proofs for higher order store programs

Describes a project that uses

Uses Software

• Smallfoot
• HIP
• Crowfoot
• VeriFast

This page was built for publication: Crowfoot: A Verifier for Higher-Order Store Programs

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