Symbolic execution proofs for higher order store programs
From MaRDI portal
Publication:287265
DOI10.1007/s10817-014-9319-8zbMath1356.68145OpenAlexW2155062053WikidataQ113901253 ScholiaQ113901253MaRDI QIDQ287265
Ben Horsfall, Bernhard Reus, Nathaniel Charlton
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
separation logicprogram verificationautomated verificationhigher order storerecursion through the store
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- 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
- Elements of generalized ultrametric domain theory
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- 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
- Characteristic formulae for the verification of imperative programs
- Compositional shape analysis by means of bi-abduction
- Mutatis mutandis
- 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
- Programming Languages and Systems
- Tools and Algorithms for the Construction and Analysis of Systems
This page was built for publication: Symbolic execution proofs for higher order store programs
