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.

You can download Eldarica from the following link.

• (October 2012): (JAR file) (sp-1429)
• (January 2013): (JAR file) (sp-1799)
• (March 2013): (JAR file) (sp-1930)
• (July 2013): (JAR file) (sp-2063)
• (February 2014): (JAR file) (sp-2305)

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.

• Nts benchmarks.
• Flata.
• Some Horn clauses.
• Non-recursive Horn benchmarks.
• Parametric Time Automata Horn benchmarks.
• Horn clauses in SMT-LIB format.

• 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

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