Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitlePolynomial approximations of the relational semantics of imperative programs
Author(s) Michael A. Colón
TypeArticle in Journal
AbstractWe present a static analysis that approximates the relational semantics of imperative programs by systems of low-degree polynomial equalities. Our method is based on Abstract Interpretation in a lattice of polynomial pseudo ideals finite-dimensional vector spaces of degree-bounded polynomials that are closed under degree-bounded products. For a fixed degree bound, the sizes of bases of pseudo ideals and the lengths of chains in the lattice of pseudo ideals are bounded by polynomials in the number of program variables. Despite the approximate nature of our analysis, for several programs taken from the literature on non-linear polynomial invariant generation our method produces results that are as precise as those produced by methods based on polynomial ideals and Gröbner bases.
KeywordsProgram analysis, Relational semantics, Abstract Interpretation, Polynomial invariants, Non-linear invariants, Polynomial ideals
URL http://www.sciencedirect.com/science/article/pii/S0167642306001584
JournalScience of Computer Programming
Pages76 - 96
NoteSpecial issue on the 11th Static Analysis Symposium - SAS 2004
Translation No
Refereed No