Skip to content
<open-source>
Oeiuwq Faith Blog OpenSource Porfolio

uuverifiers/eldarica

The Eldarica model checker
Source code at GitHub https://github.com/uuverifiers/eldarica
uuverifiers/eldarica.json
{
  "createdAt": "2014-07-20T22:34:04Z",
  "defaultBranch": "master",
  "description": "The Eldarica model checker",
  "fullName": "uuverifiers/eldarica",
  "homepage": "",
  "language": "Scala",
  "name": "eldarica",
  "pushedAt": "2025-11-25T15:53:00Z",
  "stargazersCount": 98,
  "topics": [
    "horn-clauses",
    "model-checker",
    "prolog",
    "smt-solver",
    "smt2",
    "verification"
  ],
  "updatedAt": "2025-11-25T14:42:38Z",
  "url": "https://github.com/uuverifiers/eldarica"
}

Eldarica

Section titled “Eldarica”

Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs. Inputs can be read in a variety of formats, including SMT-LIB 2 and Prolog for Horn clauses, and fragments of Scala and C for software programs, and are analysed using a variant of the Counterexample-Guided Abstraction Refinement (CEGAR) method. Eldarica is fast and includes sophisticated interpolation-based techniques for synthesising new predicates for CEGAR, enabling it to solve a wide range of verification problems.

The Eldarica C parser accepts programs augmented with various primitives from the timed automata world: supporting concurrency, clocks, communication channels, as well as analysis of systems with an unbounded number of processes (parameterised analysis).

There is also a variant of Eldarica for analysing Petri nets: http://www.philipp.ruemmer.org/eldarica-p.shtml

Eldarica has been developed by Hossein Hojjat and Philipp Ruemmer, with further contributions by Zafer Esen, Filip Konecny, and Pavle Subotic.

There is a simple web interface to experiment with the C interface of Eldarica: https://eldarica.org/eldarica

Documentation

Section titled “Documentation”

You can either download a binary release of Eldarica, or compile the Scala code yourself. Since Eldarica uses sbt, compilation is quite simple: you just need sbt installed on your machine, and then type sbt assembly to download the compiler, all required libraries, and produce a binary of Eldarica.

After compilation (or downloading a binary release), calling Eldarica is normally as easy as saying

./eld regression-tests/horn-smt-lib/rate_limiter.c.nts.smt2

When using a binary release, one can instead also call

java -jar target/scala-2.*/Eldarica-assembly*.jar regression-tests/horn-smt-lib/rate_limiter.c.nts.smt2

A set of examples is provided on https://eldarica.org/eldarica, and included in the distributions directory regression-tests.

You can use the script eld-client instead of eld in order to run Eldarica in a server-client mode, which significantly speeds up processing of multiple problems.

A full list of options can be obtained by calling ./eld -h.

The options -disj, -abstract, -stac can be used to control predicate generation. For the option -stac to work, it is currently necessary to have Yices (version 1) installed, as this is a dependency of the Flata library.

The option -sym can be used to switch to the symbolic execution engine of Eldarica, which will then be applied instead of CEGAR.

Papers

Section titled “Papers”
Section titled “Related Links”