  We propose an approach and a subsequent extension for reversing imperative
programs. Firstly, we produce both an augmented version and a corresponding
inverted version of the original program. Augmentation saves reversal
information into an auxiliary data store, maintaining segregation between this
and the program state, while never altering the data store in any other way
than that of the original program. Inversion uses this information to revert
the final program state to the state as it was before execution. We prove that
augmentation and inversion work as intended, and illustrate our approach with
several examples. We also suggest a modification to our first approach to
support non-communicating parallelism. Execution interleaving introduces a
number of challenges, each of which our extended approach considers. We define
annotation and redefine inversion to use a sequence of statement identifiers,
making the interleaving order deterministic in reverse.
