From this page you can download the current version of LEAP as a compiled binary for Linux or Mac. As it implements decision procedures on top of SMT solvers, in order to run LEAP you will need Z3 and Yices to be installed in your system and reachable through your PATH environment variable.

IMPORTANT: LEAP is currently compatible with Yices version 1.x. We are working in making LEAP compatible with Yices2. Using Yices2 will make LEAP to fail.

Compiled binaries available for:

Parametrized Invariant Generation

In collaboration with Sriram Sankaranarayanan and Bor-Yuh Evan Chang from the University of Colorado Boulder, we developed a invariant generation method for parametrized systems. Further information can be found on this paper:

The binaries and the examples used for obtaining the results presented in the paper can be downloaded from here: