Crowfoot: A Verifier for Higher-Order Store Programs

DOI10.1007/978-3-642-27940-9_10zbMath1325.68143OpenAlexW174943245MaRDI QIDQ2891407

Ben Horsfall, Nathaniel Charlton, 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

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

Related Items (2)

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

Uses Software

• VeriFast
• Crowfoot
• HIP
• Smallfoot

Cites Work

• An observationally complete program logic for imperative higher-order functions
• Specification Patterns and Proofs for Recursion through the Store
• Hoare type theory, polymorphism and separation
• A Semantic Foundation for Hidden State
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Certified assembly programming with embedded code pointers
• Automated Verification of Shape and Size Properties Via Separation Logic
• Programming Languages and Systems

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