The original aim of the GUSTT project was to combine slicing and transformation, creating a unified approach which overcomes both these problems. More specifically, GUSTT showed how domain information could be used to guide the selection of suitable slicing criteria. GUSTT defined transformations, which are used to improve the simplification power of slicing. The combined approach of slicing plus transformation is more powerful than the sum of its parts.

During the GUSTT project, it became clear that formal proof of the transformations could not be achieved by hand without significant human effort. We found that it was possible to formulate the semantics of the transformation language within the Type-theoretical constraints of the Coq proof checking system. This additional work allowed us to formulate and prove correct many transformations and our basic slicing algorithm. Importantly, it also allowed us to mechanically check our proofs.

Prof Mark Harman