Specification patterns and proofs for recursion through the store

DOI10.1007/978-3-642-22953-4_27zbMATH Open1342.68207OpenAlexW208084060MaRDI QIDQ3088293FDOQ3088293

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

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• An observationally complete program logic for imperative higher-order functions
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Certified assembly programming with embedded code pointers
• Title not available (Why is that?)
• The Mechanical Evaluation of Expressions
• Separation logic, abstraction and inheritance

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

Uses Software

• VeriFast
• Crowfoot
• Smallfoot
• jStar

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)