Giovanni Fabbretti

Reversible systems are naturally endowed with the capability of executing both forwards and backwards. Being able to execute backwards comes useful in many different ways: debugging, error-recovery, design of sound programming primitives, etc.

Most programming languages are not designed with reversibility in mind and thus lack the ability to undo their actions. The issue is that most programming languages allow functions whose inverse does not exist. However, this issue can be overcome by employing memories to save the program state before performing each action, so that, upon necessity, memories can be looked up to restore a past state.

This thesis explores the following two paths. First, we provide an implementation of the general approach proposed by Lanese and Medić to derive reversible semantics starting from non-reversible ones for concurrent systems. Then, we investigate possible notions of reversibility in settings where some memories may be lost as a side effect of some events. In particular, the case study we chose is distributed systems and the events that cause the memory loss are failures.