Linear Programming Invariant Generator

     [Latest]    [Download]    [Papers]      [Credits]


09/19/2006 Compiles under latest version of PPL (v0.9).
1/31/2005 Source Code Released. Please email us if you require installation assistance.
1/17/2005 Releasing LPInv as a supplement to our [SSM05] paper.





LPINV has been successfully compiled on i386 machines running linux. It requires the following libraries:

Library Name Version Compiled Download URL License
GNU Multi-precision Library (GMP) latest LGPL
GNU Linear Programming Kit (GLPK) 4.8 GPL
Parma Polyhedra Library (PPL) 0.9 GPL

To install please follow the steps as outlined below:




[SSM05] Sriram Sankaranarayanan, Henny Sipma and Zohar Manna, "Scalable Analysis of Linear Systems using Mathematical Programming", Verification, Model-Checking, and Abstract-Interpretation, Vol. 3385 of Lecture Notes in Computer Science, pages 21-47, January, 2005.
[MP95] Zohar Manna and Amir Pnueli, "The Temporal Verification of Reactive Systems: Safety", 1996.
[FAST] The FAST project page at
[PPL] The Parma Polyhedra Library project page at




The code was designed and implemented by Sriram Sankaranarayanan.

The key algorithms behind is joint work by Sriram Sankaranarayanan, Henny Sipma and Zohar Manna.

The project uses the PPL, GLPK and the GMP libraries at its core for which we are extremely grateful.

Thanks to Michael Colon, Aaron Bradley, Matteo Slanina and Cesar Sanchez for their ideas and suggestions.

Special thanks to Roberto Bagnara for helping us with various issues including licensing.

This project was partially funded by the NSF-EHS program (grant CCR-02-20134), by the NSF-ITR program (grant CCR-01-21403) and by the DARPA SEC program (ARPA/AF contract F33615-99-C-3014).

This page has been designed and is being maintained by Sriram Sankaranarayanan.
Questions and comments are welcome!