# Reversing Parallel Programs with Blocks and Procedures

arXiv: https://arxiv.org/abs/1808.08651 · HTML: https://mlsanity.com/paper/1808.08651/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Aug 2018.

## Built on by (most cited first, 1 of 1)

- [Executable Interval Temporal Logic Specifications](https://mlsanity.com/paper/2105.03375/) (2021)

## Abstract (arXiv)

We show how to reverse a while language extended with blocks, local variables, procedures and the interleaving parallel composition. Annotation is defined along with a set of operational semantics capable of storing necessary reversal information, and identifiers are introduced to capture the interleaving order of an execution. Inversion is defined with a set of operational semantics that use saved information to undo an execution. We prove that annotation does not alter the behaviour of the original program, and that inversion correctly restores the initial program state.