Linear Programming Invariant Generator

Latest

Download

• Tar Gzipped Sources lpinv-src.tgz.
• Precompiled binaries linux 2.6 lpinv-bin.tgz
• Examples only lpinv-examples.tgz.

Instructions

Library Name	Version Compiled	Download URL	License
GNU Multi-precision Library (GMP)	latest	http://swox.com/gmp/#DOWNLOAD	LGPL
GNU Linear Programming Kit (GLPK)	4.8	ftp://ftp.gnu.org/gnu/glpk/	GPL
Parma Polyhedra Library (PPL)	0.9	ftp://ftp.cs.unipr.it/pub/ppl/releases/	GPL

To install please follow the steps as outlined below:

• Download and install the libraries mentioned above. If installing locally, edit the LD_LIBRARY_PATH environment variable to include the install directories.
• Go to $(LPINV_PATH)/src/ and edit Makefile.globals to fill in the correct path information. If you have installed the library globally in a place where gcc sees them automatically, (eg., /usr/lib or /usr/include ) just replace all the paths with blanks.

  ##

  ## The location of your include files

  ##

  PPL_INCLUDE = /directory/of/ppl.hh

  GLPK_INCLUDE = /directory/of/glpk.h

  GMP_INCLUDE = /directory/of/gmp.h

  ##

  ## The location of your librarires

  ##

  GMP_LIB = /path/to/libgmp

  PPL_LIB = /path/to/libppl

  GLPK_LIB = /path/to/libglpk

• You can now compile by typing "make".
• If your compilation went OK, you should obtain three executables.
  
  • lpinv: Drives all examples under $(LPINV_PATH)/examples/Standard/
  • lpinv-delz: Drives all examples under $(LPINV_PATH)/examples/Delz/.

References

  

[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 http://www.lsv.ens-cachan.fr/fast.
[PPL]	The Parma Polyhedra Library project page at http://www.cs.unipr.it/ppl.

  

  

Credits

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!