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 ·x2 -2x3 = 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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Müller-Olm, M., Petter, M., & Seidl, H. (2006). Interprocedurally analyzing polynomial identities. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3884 LNCS, pp. 50–67). Springer Verlag. https://doi.org/10.1007/11672142_3
Mendeley helps you to discover research relevant for your work.