University of Sussex
Browse
paper.pdf (746.07 kB)

Symbolic execution proofs for higher order store programs

Download (746.07 kB)
journal contribution
posted on 2023-06-08, 20:19 authored by Bernhard ReusBernhard Reus, Nathaniel Charlton, Ben Horsfall
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.

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 Reasoning

ISSN

0168-7433

Publisher

Springer Verlag

Issue

3

Volume

54

Page range

199-284

Department affiliated with

  • Informatics Publications

Full text available

  • Yes

Peer reviewed?

  • Yes

Legacy Posted Date

2015-03-13

First Open Access (FOA) Date

2016-03-01

First Compliant Deposit (FCD) Date

2015-03-13

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC