Polyrank
Description
Polyrank analyzes the termination of numerical loops. This
release consists of implementations of the finite difference
approach for loops with polynomial assignments and guards and the
synthesis of polyranking functions for loops with linear
transition relations. The latter method subsumes linear ranking
function synthesis. The tools accept abstract descriptions of loops.
Our C loop abstraction tool is not ready for general release.
The code is released under the GNU GENERAL PUBLIC
LICENSE.
Downloading
Look at the README to see what you're
getting into.
Download binaries (compiled on
Linux 2.4.2 for i386).
Or download the source code.
All material is copyright (c) 2005 Aaron R. Bradley.