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.
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.