Interproc is an interprocedural analyzer for a small imperative language with (recursive) procedure calls. It infers invariants on the numerical variables of analyzed program.
It it intended as a pedagogical and experimental tool. It also demonstrates the features of the APRON library and the use of the Fixpoint libraries.
It is implemented in OCaml.
Interproc itself is released under LGPL license (GNU General Public License).
You can play with Interproc online.