Specification Patterns and Proofs for Recursion through the Store

DOI10.1007/978-3-642-22953-4_27zbMath1342.68207OpenAlexW208084060MaRDI QIDQ3088293

Nathaniel Charlton, Bernhard Reus

Publication date: 19 August 2011

Published in: Fundamentals of Computation Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22953-4_27

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (3)

Crowfoot: A Verifier for Higher-Order Store Programs ⋮ Symbolic execution proofs for higher order store programs ⋮ Specification patterns for reasoning about recursion through the store

Uses Software

• VeriFast
• Crowfoot
• Smallfoot
• jStar

Cites Work

• An observationally complete program logic for imperative higher-order functions
• Separation logic, abstraction and inheritance
• 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
• The Mechanical Evaluation of Expressions
• Unnamed Item
• Unnamed Item

This page was built for publication: Specification Patterns and Proofs for Recursion through the Store