Pater

Pater (Policy iteration-based Analysis for TERmination) is a small analyzer to prove termination of loops with real variables based on the application of policy iteration to abstract interpretation (based on my VMCAI'14 paper). It is written in OCaml and uses the Verimag Polyhedra Library (VPL) to handle polyhedra and linear programming.

The source code, as well as the examples, is available here. To compile it you need:

• OCaml (recent version) with ocamlfind

• VPL library (VPL)

• gmp (with ocaml interface) and zarith (needed for VPL)

Warning: this program is no longer maintained. I am currently writing a new analyzer with a better interface.