Symbolic execution proofs for higher order store programs
DOI10.1007/S10817-014-9319-8zbMATH Open1356.68145OpenAlexW2155062053WikidataQ113901253 ScholiaQ113901253MaRDI QIDQ287265FDOQ287265
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
Recommendations
automated verificationprogram verificationseparation logichigher order storerecursion through the store
Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Cites Work
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Characteristic formulae for the verification of imperative programs
- Elements of generalized ultrametric domain theory
- Programming Languages and Systems
- Crowfoot: A Verifier for Higher-Order Store Programs
- Effective interactive proofs for higher-order imperative programs
- Specification patterns and proofs for recursion through the store
- Nested Hoare triples and frame rules for higher-order store
- Hoare type theory, polymorphism and separation
- A semantic foundation for hidden state
- Separation Logic for Higher-Order Store
- Nested Hoare Triples and Frame Rules for Higher-Order Store
- 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
- Compositional shape analysis by means of bi-abduction
- Mutatis mutandis: safe and predictable dynamic software updating
- Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
- Programming Languages and Systems
- Certified assembly programming with embedded code pointers
- A proof system for separation logic with magic wand
- Step-indexed Kripke models over recursive worlds
- Title not available (Why is that?)
- 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
Uses Software
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)
