Equality saturation : engineering challenges and applications

In this dissertation, I describe the Peggy system for performing program optimization and translation validation. Peggy is based on the concept of Equality Saturation, in which axiomatic reasoning is applied to a program to produce exponentially many equivalent versions of that program, which can then be explored simultaneously. This is achieved by using a custom intermediate representation that facilitates mathematical reasoning over programs. I will specifically address some of the engineering challenges posed by making a working implementation of the Equality Saturation technique, as well as the major applications to which we have applied it. I implemented front-ends for Peggy to convert both Java bytecode programs and LLVM programs to and from our custom intermediate representation. I designed and implemented a domain-specific language for writing the axioms that are used by the Equality Saturation engine. For the purposes of optimization, I designed the technique whereby we choose the optimal program from our representation of exponentially many equivalent programs. I implemented both our optimization and our translation validation frameworks that use the Equality Saturation engine. In addition, I performed experiments showing the effectiveness of Equality Saturation at both program optimization and translation validatio