Sequential, Parallel, and Quantified Updates of First-Order Structures

We present a datastructure for storing memory contents of imperative programs during symbolic execution---a technique frequently used for program verification and testing. The concept, called updates, can be integrated in dynamic logic as runtime infrastructure and models both stack and heap. Here, updates are systematically developed as an imperative programming language that provides the following constructs: assignments, guards, sequential composition and bounded as well as unbounded parallel composition. The language is equipped both with a denotational semantics and a correct rewriting system for execution, whereby the latter is a generalisation of the syntactic application of substitutions. The normalisation of updates is discussed. All results and the complete theory of updates have been formalised and proven using the Isabelle/HOL proof assistant