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 non-concurrent systems.

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 C-like 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 single-linked 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