Markus Müller-Olm, Helmut Seidl and Bernhard Steffen. Interprocedural Herbrand Equalities. In Shmuel Sagiv, editor, Programming Languages and Systems, volume 3444 of Lecture Notes in Computer Science, pages 31-45, Edinburgh, UK, April 2005. Springer.

We present an aggressive interprocedural analysis for inferring value equalities which are independent of the concrete interpretation of the operator symbols. These equalities, called Herbrand equalities, are therefore an ideal basis for truly machine-independent optimizations as they hold on every machine. Besides a general correctness theorem, covering arbitrary call-by-value parameters and local and global variables, we also obtain two new completeness results: one by constraining the analysis problem to Herbrand constants, and one by allowing side-effect-free functions only. Thus if we miss a constant/equality in these two scenarios, then there exists a separating interpretation of the operator symbols.

Download: PDF Reference: Bibtex The original publication is available at