Helmut Seidl, Andrea Flexeder and Michael Petter. **Analysing All Polynomial Equations in **. 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 . In contrast to the infinite field , 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 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 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