Introduction
LEAP is a deductive verification tool under development at the IMDEA Software Institute which aims the verification of temporal properties in concurrent parametrized systems, specially the ones that dynamically modify the heap by manipulating complex data structures.
Currently, LEAP supports the verification of both safety and liveness properties. Despite is main target is concurrent systems, it can also be used to analyze nonconcurrent systems.
NEW! Now it is possible to try LEAP online at this website.
LEAP is written in Ocaml and it is constructed modularly. When performing the analysis of safety properties, LEAP needs as input a program described in a Clike language, a set of invariant candidates and a proof graph describing the interdependency between the invariant candidates. In the case of liveness properties, LEAP requires as input a program, a representation of the parametrized verification diagram representing the proof and optionally a collection of supporting invariants.
For performing the analysis of the parametrized temporal properties, LEAP implements specialized techniques. All these techniques implemented by LEAP reduce the verification problem of a parametrized system to a finite collection of verification conditions. Finally, the validity of each generated verification condition can be verified using a suitable decision procedure. Because of that, currently LEAP implements six different decision procedures, constructed on top of SMT solvers such as Z3, Yices and CVC4:
 a decision procedure that can reason only about first order logic formulas and program locations, considering all other predicates as uninterpreted.
 a decision procedure that reasons about program locations, integers and finite sets of integers with minimum and maximum functions.
 a decision procedure that reasons about program locations, integers, finite sets of integers with minimum and maximum functions and pairs of integers and thread identifiers.
 a decision procedure based on TLL capable of reasoning about singlelinked lists layouts in the heap with locks.
 a decision procedure based on TSLK capable of reasoning about skiplists of height K.
 a decision procedure based on TSL which can deal with skiplist of an unbounded number of levels
The modular approach of LEAP makes it simple to be extensible for new program languages and theories. The schematic construction of the tool can be described as follows:
References

Parametrized Invariance for Infinite State Processes
Alejandro Sánchez and César Sánchez
Acta Informatica, 2015

Parametrized Verification Diagrams
Alejandro Sánchez and César Sánchez
21st International Symposium on Temporal Representation and Reasoning (TIME), 2014

LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes
Alejandro Sánchez and César Sánchez
26th International Conference on Computer Aided Verification (CAV), 2014

Formal Verification of Skiplists with Arbitrarily Many Levels
Alejandro Sánchez and César Sánchez
12th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2014

A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes
Alejandro Sánchez and César Sánchez 3rd International Symposium of NASA Formal Methods (NFM), 2011

Decision Procedures for the Temporal Verification of Concurrent Lists
Alejandro Sánchez and César Sánchez
12th International Conference on Formal Engineering Methods (ICFEM), 2010