LARA

This is an old revision of the document!


ELDARICA


NEW: GitHub link: https://github.com/uuverifiers/eldarica


A real Eldarica Tree A reachability tree created by Eldarica for the
mutual exclusion protocol with arbitrary number of clients



Eldarica Eldarica is a predicate abstraction engine. It generates the abstract reachability tree (ART) using lazy abstraction with Cartesian abstraction. It uses the Princess interpolating prover to refine the set of predicates. Besides Princess, Eldarica is able to use Z3 as a theorem prover for constructing an abstraction of the program. For the Z3 connection, Eldarica uses ScalaZ3.

Eldarica can take as input a subset of Scala, or logical representations such as Numerical Transition Systems and Horn clauses.

Download


You can download Eldarica from the following link.

Running


  • Verification of the horn benchmark FILENAME.horn: java -jar eldarica.jar FILENAME.horn -horn -hin -princess
  • Verification of the horn benchmark FILENAME.horn using the bottom-up approach: java -jar eldarica.jar FILENAME.horn -horn -hin -princess -bup
  • Verification of the nts benchmark FILENAME.nts: java -jar eldarica.jar FILENAME.nts -i -princess
  • Verification of the nts benchmark FILENAME.nts using conversion to Horn clauses: java -jar eldarica.jar FILENAME.horn -horn -princess
  • Converting the nts benchmark FILENAME.nts to Horn clauses: java -jar eldarica.jar FILENAME.nts -horn -p

Authors


Eldarica is being developed and maintained at LARA by Hossein Hojjat with contributions from Philipp Ruemmer and Filip Konecny.