NOTE: this version of LEAP is still experimental, documentation may be out of date.
LEAP is a prototype theorem prover which aims the formal verification of temporal properties, both safety and liveness, of parametrized programs. In particular, LEAP is designed for the analysis of programs that manipulate concurrent data types that store both finite and infinite data.
LEAP receives as input an annotated program and a temporal specification. As output, it states whether the temporal specification holds under the assumption of an unbounded number of threads executing the input program. To accomplish this, in its core LEAP implements:
-
A collection of specialized deductive proof rules which reduce the verification problem to a finite collection of verification conditions, whose validity entails the satisfaction of the temporal specification by the parametrized system.
-
A set of decision procedures, which can automatically verify the validity of the previously generated verification conditions.
LEAP is available as source code and as binaries for Linux and Mac. Since LEAP works of top of some SMT solvers, you will need to install at least:
- Get the source code
git clone https://github.com/imdea-software/leap - Compile LEAP
make leap(requires ocamlbuild and ocaml >= 4.02.0)
Examples, tutorials and compiled binaries for Linux and Mac are available from LEAP's website. In particular, there exists binary versions for:
Examples can also be found in the examples folder of this repository.
NEW! LEAP can now be used at its online website.
There exists a tutorial at LEAP's website.
It is possible to check whether LEAP was successfully installed by executing leap -version, which output the current LEAP version.
A list of available options can be obtained by executing leap -help. Further details about command line options and the methodology for using LEAP can be found in the examples folder of this repository and in chapter 9 of Alejandro Sanchez's PhD Thesis.
A comprehensive presentation of LEAP can be found in chapter 9 of Alejandro Sanchez's PhD Thesis.
LEAP implementation is based on the following publications:
- Parametrized Invariance for Infinite State Processes, which introduces the parametrized invariance proof rules for safety properties (Acta Informatica 2015).
- Parametrized Verification Diagrams, which describes a diagram based method which enables the parametrized verification of liveness properties (TIME 2014).
- LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes, which briefly introduces the functionalities offered by LEAP (CAV 2014).
- Formal Verification of Skiplists with Arbitrarily Many Levels, which describes a decision procedure for skiplists with an unbounded number of levels (ATVA 2014).
- A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes, which presents a decision procedure for families of skiplists with a bounded number of levels (NFM 2011).
- Decision Procedures for the Temporal Verification of Concurrent Lists, which describes a decision procedure for data structures of the shape of concurrent lists (ICFEM 2010).
LEAP is currently developed and maintained by: