Helmut Seidl, Andrea Flexeder and Michael Petter. Analysing All Polynomial Equations in ${\mathbb Z_{2^w}}$ . In María Alpuente and Germán Vidal, editors, Static Analysis, volume 5079 of Lecture Notes in Computer Science, pages 299-314, Valencia, Spain, July 2008. Springer.

In this paper, we present methods for checking and inferring all valid polynomial relations in ${\mathbb Z_{2^w}}$ . In contrast to the infinite field ${\mathbb{Q}}$ , ${\mathbb Z_{2^w}}$ is finite and hence allows for finitely many polynomial functions only. In this paper we show, that checking the validity of a polynomial invariant over ${\mathbb Z_{2^w}}$ is, though decidable, only PSPACE-complete. Apart from the impracticable algorithm for the theoretical upper bound, we present a feasible algorithm for verifying polynomial invariants over ${\mathbb Z_{2^w}}$ which runs in polynomial time if the number of program variables is bounded by a constant. In this case, we also obtain a polynomial-time algorithm for inferring all polynomial relations. In general, our approach provides us with a feasible algorithm to infer all polynomial invariants up to a low degree.

Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com