@inproceedings{ff231958037049e79f4afca7c4aa834f,
title = "Interprocedurally analyzing polynomial identities",
abstract = "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.",
author = "Markus M{\"u}ller-Olm and Michael Petter and Helmut Seidl",
year = "2006",
doi = "10.1007/11672142_3",
language = "English",
isbn = "3540323015",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "50--67",
booktitle = "STACS 2006",
note = "STACS 2006: 23rd Annual Symposium on Theoretical Aspects of Computer Science, Proceedings ; Conference date: 23-02-2006 Through 25-02-2006",
}