Lab for Automated Reasoning and Analysis LARA

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.

We have released the Eldarica source code under the BSD 3-Clause license on Github. We won't post the new releases in this webpage anymore.

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.

 
eldarica.txt · Last modified: 2014/09/23 17:16 by hossein