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.