Executive Summary : | This proposal aims to develop a new algorithm for computing Herbrand Equivalence of expressions in computer programs using fixpoint theory of monotone functions over complete lattices. A flow graph is defined with nodes representing statements in the program and directed edges connecting two nodes. Two expressions are said to be Herbrand equivalent at p if they assume syntactically the same value at p, regardless of the path in the flow graph. Kildall's method in 1973 iterates over the flow graph and maintains equivalence classes of all possible expressions. However, this method requires exponential time and space complexity. Later algorithms improved efficiency by restricting the domain of expressions and computing a subset of relevant equivalences. The classical definition of Herbrand Equivalence is based on a Meet Over All Paths (MOP) characterisation, but all algorithms are fix point-based methods. A recent joint work involving the author formulated a lattice theoretic framework, showing that Herbrand Equivalence at program points is the maximum fix point of a composite transfer function on a relevant complete lattice. This new definition is equivalent to the MOP definition. However, since the lattice must be infinite, an algorithm for computing Herbrand equivalence cannot be directly derived from it. An efficient method for abstract interpretation of the composite transfer function presented in the previous work can be used to derive a polynomial time algorithm for computing Herbrand equivalence of expressions of length at most two at each program point. |