Symbolic execution proofs for higher order store programs

DOI10.1007/S10817-014-9319-8MaRDI QIDQ287265zbMATH OpenOpenAlexWikidataFDO

Authors Bernhard Reus, Nathaniel Charlton, Ben Horsfall

Publication date 26 May 2016

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL http://sro.sussex.ac.uk/id/eprint/53364/2/paper.pdf

zbMATH Keywords

automated verificationprogram verificationseparation logichigher order storerecursion through the store

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Hoare logic for higher order store using simple semantics
• Automata, Languages and Programming
• Crowfoot: A Verifier for Higher-Order Store Programs
• Nested Hoare triples and frame rules for higher-order store
• Nested Hoare Triples and Frame Rules for Higher-Order Store

Cites work

• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• A proof system for separation logic with magic wand
• A semantic foundation for hidden state
• An observationally complete program logic for imperative higher-order functions
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Certified assembly programming with embedded code pointers
• Characteristic formulae for the verification of imperative programs
• Compositional shape analysis by means of bi-abduction
• Crowfoot: A Verifier for Higher-Order Store Programs
• Effective interactive proofs for higher-order imperative programs
• Elements of generalized ultrametric domain theory
• Hoare type theory, polymorphism and separation
• Mutatis mutandis: safe and predictable dynamic software updating
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Nested Hoare triples and frame rules for higher-order store
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Programming Languages and Systems
• Programming Languages and Systems
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Separation Logic for Higher-Order Store
• Specification patterns and proofs for recursion through the store
• Step-indexed Kripke models over recursive worlds
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(6)

• Hoare logic for higher order store using simple semantics
• Specification patterns and proofs for recursion through the store
• Nested Hoare triples and frame rules for higher-order store
• Automata, Languages and Programming
• Higher order symbolic execution for contract verification and refutation
• Crowfoot: A Verifier for Higher-Order Store Programs

Describes a project that uses

Uses Software

• CFML
• jStar
• Smallfoot
• HIP
• Crowfoot
• VeriFast

This page was built for publication: Symbolic execution proofs for higher order store programs

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