Skip to content

mattulbrich/eldarica

 
 

Repository files navigation

Eldarica

Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and Scala programs. Inputs can be read in a variety of formats, including SMT-LIB 2 and Prolog for Horn clauses, 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.

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

There is a simple web interface to experiment with the C interface of Eldarica: http://logicrunch.it.uu.se:4096/~wv/eldarica

The latest nightly build is available from: http://logicrunch.it.uu.se:4096/~wv/eldarica/eldarica-bin-nightly.zip

Documentation

You can either download a binary release of Eldarica, or compile the Scala code yourself. For the latter, you need a recent Scala compiler, and set the environment variable SCALA_HOME to point to the directory of the Scala distribution. After that you can simply call ant to start the build.

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

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.
In particular, the options -disj, -abstract, -stac can be used to control predicate generation.

Papers

Related Links

Build Status

About

The Eldarica model checker

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Scala 70.8%
  • SMT 27.6%
  • Lex 0.6%
  • Shell 0.4%
  • Makefile 0.4%
  • C 0.1%
  • Smarty 0.1%