Symbolic execution proofs for higher order store programs

Reus, Bernhard, Charlton, Nathaniel and Horsfall, Ben (2015) Symbolic execution proofs for higher order store programs. Journal of Automated Reasoning, 54 (3). pp. 199-284. ISSN 0168-7433

PDF - Accepted Version
Download (763kB) | Preview


Higher 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.

Item Type: Article
Keywords: Program verification; Higher order store; Recursion through the store; Separation logic; Automated verification
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Related URLs:
Depositing User: Bernhard Reus
Date Deposited: 13 Mar 2015 13:48
Last Modified: 07 Mar 2017 09:41

View download statistics for this item

📧 Request an update
Project NameSussex Project NumberFunderFunder Ref
From Reasoning Principles for Function Pointers To Logics for Self-Configuring ProgramsUnsetEPSRCEP/G003173/1