FUTHER CONSIDERATION ON THE FORMAL VERIFICATION OF NUMBER THERETICAL ALGORITHMS
Laura Kovács, Adalbert Kovács · 2009
We discuss experimental results of an automatic approach for inferring polynomial loop invariants of P-solvable loops implementing interesting number- theoretic algorithms. The method relies on techniques from symbolic summation and polynomial algebra, and is implemented in the software package Aligator written in Mathematica.