Nested Hoare Triples and Frame Rules for Higher-order Store

DOI10.2168/LMCS-7(3:21)2011zbMath1237.68066MaRDI QIDQ3224687

Hongseok Yang, Bernhard Reus, Lars Birkedal, Jan Schwinghammer

Publication date: 2 April 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

semanticsHoare logicseparation logichigher-order store

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) 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

• Crowfoot
• Ynot

This page was built for publication: Nested Hoare Triples and Frame Rules for Higher-order Store