Isomorphism and Program Equivalence

Tim will talk about two related pieces of work. Both use the idea of isomorphism as a means of understanding program modifications.

Program Equivalence From Trace Equivalence: Joint work with Sophia Drossopoulou

Often when programmers modify source code they intend to preserve some parts of the program behaviour. We propose a formal criterion by which to characterise the preserved part of the program behaviour. Two program versions are equivalent up to a set of affected objects A, if executions of the two versions correspond at each execution step when we do not consider the objects in A. We propose a sufficient condition for this criterion, which is useful for a tool we are building. It suffices to establish that traces of method calls and returns between A objects and other objects are equivalent. Examining the stack and heap at each execution step is not necessary. We give a proof of the sufficiency of this condition, much of which we have automatically verified using Dafny. We also discuss our experiences with Dafny.

Heap Isomorphism for Modular Program Equivalence Checking: Joint work with Shuvendu Lahiri, Sophia Drossopoulou

Modular verification of program equivalence typically involves equating the pre and post states of two versions of a procedure. We call this equivalence up to equality. Verification of equivalence up to equality succeeds if the same post state is produced, from the same pre state, by each version. Equivalence up to equality verification has been particularly successful in compiler translation validation. It is common to model the heap as arrays and require that these arrays are equal across procedure calls.

However, a number of challenges remain before program equivalence checking technologies are ready for widespread use. One problem is to verify equivalence between program versions in the presence of the heap and dynamic memory allocation. We address two aspects of this problem:

A notion of equivalence in the presence of non-deterministic allocation, reordering of allocations, or other differences in memory allocation. We call this equivalence up to isomorphism. – a method for performing such equivalence checking modularly in the presence of loops and recursion — which can produce unbounded state updates. We use Boogie to implement automatic verification of equivalence up to isomorphism.

Speaker Bios

Tim Wood is a PhD student at Imperial College London supervised by Prof. Sophia Drossopoulou. His research is focused on tools to help programmers change software safely and quickly. He spent the previous decade working as a software engineer designing and building highly available telecoms networks.