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.
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.
Eldarica is being developed and maintained at LARA by
Hossein Hojjat with contributions from Philipp Ruemmer and Filip Konecny.