paper.pdf (746.07 kB)
Symbolic execution proofs for higher order store programs
journal contribution
posted on 2023-06-08, 20:19 authored by Bernhard ReusBernhard Reus, Nathaniel Charlton, Ben HorsfallHigher order store programs are programs which store, manipulate and invoke code at runtime. Important examples of higher order store programs include operating system kernels which dynamically load and unload kernel modules. Yet conventional Hoare logics, which provide no means of representing changes to code at runtime, are not applicable to such programs. Recently, however, new logics using nested Hoare triples have addressed this shortcoming. In this paper we describe, from top to bottom, a sound semi-automated verification system for higher order store programs. We give a programming language with higher order store features, define an assertion language with nested triples for specifying such programs, and provide reasoning rules for proving programs correct. We then present in full our algorithms for automatically constructing correctness proofs. In contrast to earlier work, the language also includes ordinary (fixed) procedures and mutable local variables, making it easy to model programs which perform dynamic loading and other higher order store operations. We give an operational semantics for programs and a step-indexed interpretation of assertions, and use these to show soundness of our reasoning rules, which include a deep frame rule which allows more modular proofs. Our automated reasoning algorithms include a scheme for separation logic based symbolic execution of programs, and automated provers for solving various kinds of entailment problems. The latter are presented in the form of sets of derived proof rules which are constrained enough to be read as a proof search algorithm.
Funding
From Reasoning Principles for Function Pointers To Logics for Self-Configuring Programs; EPSRC; EP/G003173/1
History
Publication status
- Published
File Version
- Accepted version
Journal
Journal of Automated ReasoningISSN
0168-7433Publisher
Springer VerlagExternal DOI
Issue
3Volume
54Page range
199-284Department affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2015-03-13First Open Access (FOA) Date
2016-03-01First Compliant Deposit (FCD) Date
2015-03-13Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC