Simplifier for Quantifier-Free Linear Arithmetical Expressions As a Means for Optimizing Automated Proofs of Partial Program Equivalence

Abstract

The purpose of this study is to introduce performance optimizations and improvements to Pequod, an implementation of an algorithm capable of proving or disproving partial equivalence of two computer programs, given their source code or compiled code, without running them. This algorithm can also be re-purposed to solve different fundamental problems, such as proving multithreaded security. Here, partial equivalence of two programs, given matching inputs, means that, if both terminate (i.e. do not loop infinitely), they produce matching outputs. Programs are viewed as sets of procedures (a Java function is an example of a procedure). The following inputs are used: two procedures A and B, one in each program, and some mapping relations correlating the inputs and outputs of A to, respectively, the inputs and outputs of B. The algorithm used in Pequod is expected to be far more robust and reliable than any of the currently existing technology for proving partial equivalence, due to being applicable to a far wider range of programs because of the properties of the underlying concept of product programs. This technology could find applications in areas such as industry, where it could be used to prove the equivalence of some well-tested implementation with a more optimal replacement, or education, where it could be used to verify correctness of students’ solutions to programming problems. With Pequod, partial equivalence proofs could extend from being usable in select specific cases to a wide range of possible situations. The optimizations being introduced to, and proposed for Pequod mostly revolve around simplifying quantifier-free linear arithmetical expressions produced during the proof process.