Hoare logic for higher order store using simple semantics

DOI10.1007/978-3-642-20920-8_10MaRDI QIDQ3003346zbMATH OpenOpenAlexFDO

Authors Nathaniel Charlton

Publication date 27 May 2011

Published in Logic, Language, Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-20920-8_10

zbMATH Keywords

higher-order storeHoare logicmodular proof

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Automata, Languages and Programming
• Symbolic execution proofs for higher order store programs
• A Simple Model of Separation Logic for Higher-Order Store
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Nested Hoare triples and frame rules for higher-order store

Cited in

(8)

• Symbolic execution proofs for higher order store programs
• Specification patterns and proofs for recursion through the store
• A Simple Model of Separation Logic for Higher-Order Store
• Separation Logic for Higher-Order Store
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Specification patterns for reasoning about recursion through the store
• Automata, Languages and Programming
• Logical Reasoning for Higher-Order Functions with Local State

This page was built for publication: Hoare logic for higher order store using simple semantics

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