Specification patterns for reasoning about recursion through the store

DOI10.1016/j.ic.2013.08.011zbMath1358.68184OpenAlexW2062653699MaRDI QIDQ393092

Bernhard Reus, Nathaniel Charlton

Publication date: 16 January 2014

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2013.08.011

zbMATH Keywords

Hoare logicseparation logichigher-order store

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• VeriFast
• Crowfoot
• Smallfoot
• jStar
• Ynot
• MiniML

Cites Work

• Unnamed Item
• Solving reflexive domain equations in a category of complete metric spaces
• Crowfoot: A Verifier for Higher-Order Store Programs
• Hoare Logic for Higher Order Store Using Simple Semantics
• Specification Patterns and Proofs for Recursion through the Store
• A modal analysis of staged computation
• Nested Hoare Triples and Frame Rules for Higher-order Store
• A Simple Model of Separation Logic for Higher-Order Store
• Hoare type theory, polymorphism and separation
• A Semantic Foundation for Hidden State
• Realisability semantics of parametric polymorphism, general references and recursive types
• Abstracting Allocation
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Ynot
• Mutatis mutandis
• Verification: Theory and Practice
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Certified assembly programming with embedded code pointers
• Step-indexed kripke models over recursive worlds
• A Realizability Model for Impredicative Hoare Type Theory
• Automata, Languages and Programming
• The Mechanical Evaluation of Expressions

This page was built for publication: Specification patterns for reasoning about recursion through the store