Markus Müller-Olm and Helmut Seidl. Computing Polynomial Program Invariants. Inf. Process. Lett., 91(5):233-244, 2004.
We present two automatic program analyses. The first analysis checks if a given polynomial relation holds among the program variables whenever control reaches a given program point. It fully interprets assignment statements with polynomial expressions on the right-hand side and polynomial disequality guards. Other assignments are treated as non-deterministically assigning any value and guards that are not polynomial disequalities are ignored. The second analysis extends this checking procedure. It computes the set of all polynomial relations of an arbitrary given form that are valid at a given target program point. It is also complete up to the abstraction described above.