====== ELDARICA ======

----

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

----

|     [[http://www.public.asu.edu/~camartin/plants/Plant%20html%20files/pinuseldarica.html|{{ eldarica.jpg?150| }}]]      |       {{reachability.png?100}}   |
| 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 [[http://www.philipp.ruemmer.org/princess.shtml|Princess]] interpolating prover to refine the set of predicates.
Besides Princess, Eldarica is able to use [[http://research.microsoft.com/en-us/um/redmond/projects/z3/|Z3]] as a theorem prover for constructing an abstraction of the program.
For the Z3 connection, Eldarica uses [[https://github.com/psuter/ScalaZ3/|ScalaZ3]].

Eldarica can take as input a subset of Scala, or logical representations such as [[http://nts.imag.fr/|Numerical Transition Systems]] and [[https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/|Horn clauses]].

==== Download ====
\\
You can download Eldarica from the following link.
  * (October 2012):  ({{eldarica-1429.jar.gz|JAR file}}) (sp-1429)
  * (January 2013):  ({{eldarica-1799.jar.gz|JAR file}}) (sp-1799)
  * (March   2013):  ({{eldarica-1930.jar.gz|JAR file}}) (sp-1930)
  * (July    2013):  ({{eldarica-2063.jar.gz|JAR file}}) (sp-2063)
  * (February 2014): ({{eldarica-2305.jar.gz|JAR file}}) (sp-2305)

We have released the Eldarica source code under the BSD 3-Clause license on [[https://github.com/uuverifiers/eldarica/|Github]].
We won't post the new releases in this webpage anymore.

==== Related Links ====
\\
  * [[http://richmodels.epfl.ch/ntscomp/ntslib|Nts]] benchmarks.
  * [[http://www-verimag.imag.fr/FLATA.html|Flata]].
  * Some {{horn-benchmarks.tar.gz|Horn}} clauses.
  * [[horn-nonrec-benchmarks|Non-recursive Horn benchmarks.]] 
  * [[horn-parametric-benchmarks|Parametric Time Automata Horn benchmarks.]] 
  * [[https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/LIA/Eldarica/|Horn clauses]] in SMT-LIB format.
==== 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 [[http://icwww.epfl.ch/~hojjat/|
Hossein Hojjat]] with contributions from [[http://www.philipp.ruemmer.org/|Philipp Ruemmer]] and Filip Konecny.