Markus Müller-Olm, Michael Petter and Helmut Seidl. Interprocedurally Analyzing Polynomial Identities. In Bruno Durand and Wolfgang Thomas, editors, 23rd Annual Symposium on Theoretical Aspects of Computer Science, volume 3884 of Lecture Notes in Computer Science, pages 50-67, Marseille, France, February 2006. Springer.

Since programming languages are Turing complete, it is impossible to decide for all programs whether a given non-trivial semantic property is valid or not. The way-out chosen by abstract interpretation is to provide approximate methods which may fail to certify a program property on some programs. Precision of the analysis can be measured by providing classes of programs for which the analysis is complete, i.e., decides the property in question. Here, we consider analyses of polynomial identities between integer variables such as $x_{1} \cdot x_{2} - 2x_{3} = 0$. We describe current approaches and clarify their completeness properties. We also present an extension of our approach based on weakest precondition computations to programs with procedures and equality guards.

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