Specification patterns and proofs for recursion through the store

DOI10.1007/978-3-642-22953-4_27MaRDI QIDQ3088293zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Specification patterns for reasoning about recursion through the store
• Automata, Languages and Programming
• Hoare logic for higher order store using simple semantics
• Symbolic execution proofs for higher order store programs
• Nested Hoare Triples and Frame Rules for Higher-Order Store

Cites work

• scientific article; zbMATH DE number 1006119 (Why is no real title available?)
• scientific article; zbMATH DE number 944097 (Why is no real title available?)
• An observationally complete program logic for imperative higher-order functions
• Certified assembly programming with embedded code pointers
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Separation logic, abstraction and inheritance
• The Mechanical Evaluation of Expressions

Cited in

(3)

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

Describes a project that uses

Uses Software

• jStar
• Smallfoot
• Crowfoot
• VeriFast

This page was built for publication: Specification patterns and proofs for recursion through the store

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