Eldarica version 2.1

Many internal changes and bugfixes, and a few new functions. The option -logPreds:P can be used to control the debugging output generated with the option -log. The symbolic execution engine has been refined, and is now used as part of the portfolio (enabled using option -portfolio).

Eldarica 2.0.9

There are various internal changes and bugfixes, in particular in the solvers for different theories. It is now possible to solve clauses with rational arithmetic constraints, although our SMT-LIB parser is not yet connected to this. An option -cloneArrays was added that makes Eldarica use a separate array theory instance for independent array arguments; this should be more efficient than the standard behavior when using arrays to model uninterpreted functions.

Eldarica 2.0.8

Various changes/improvements in the array solver, and many bugfixes.

Eldarica 2.0.7

Much of the model checking engine has been refactored since the last release, to make it easier to maintain. The theory of heap has been improved, clause preprocessing has become more powerful, and there is initial support for polymorphic ADTs.

Eldarica 2.0.6

Improved support for the theory of arrays and some theory combinations. More specifically, constant arrays and some theory combinations (e.g. arrays + ADTs) are now supported.

Eldarica 2.0.5-heap

Eldarica 2.0.5 with additional support for the theory of heap.

/heap-theory-examples/ folder contains some examples given in SMT-LIB, translated from C using TriCera except one hand-written example: motivating-example.smt2.

The examples can either be ran in batch mode using

/heap-theory-examples/runexamples

or by passing the files as an argument to Eldarica using one of the methods shown below:

./eld heap-theory-examples/typecastSafe-001.smt2
[...]
sat

or

java -jar target/scala-2.11/Eldarica-assembly-2.0.4-heap.jar heap-theory-examples/motivating-example.smt2
[...]
sat

-cex parameter can also be provided in order to display the counterexamples when the result is unsat. -ssol parameter displays the solution when the result is sat; however, the displayed solutions might currently be difficult to read.

Note that only .smt2 files should be passed to Eldarica. The .c files under /heap-theory-examples/ are provided only for reference in order to show where the encodings came from, and should not be directly passed to Eldarica. This will result in an error as Eldarica does not have support for C programs with heap interactions (see TriCera for this, but note that it is also quite experimental at this point).

We also provide some benchmarks under /heap-theory-benchmarks/ which were generated using TriCera, please see the readme inside that directory for more information.

Eldarica 2.0.5

This version includes mostly internal changes and bugfixes, feature-wise it is similar to 2.0.4.

Eldarica 2.0.4-heap

Identical to Eldarica 2.0.4 with additional support for the theory of heap.

/heap-theory-examples/ folder contains some examples given in SMT-LIB, translated from C using TriCera except one hand-written example: motivating-example.smt2.

The examples can either be ran in batch mode using

/heap-theory-examples/runexamples

or by passing the files as an argument to Eldarica using one of the methods shown below:

./eld heap-theory-examples/typecastSafe-001.smt2
[...]
sat

or

java -jar target/scala-2.11/Eldarica-assembly-2.0.4-heap.jar heap-theory-examples/motivating-example.smt2
[...]
sat

-cex parameter can also be provided in order to display the counterexamples when the result is unsat. -ssol parameter displays the solution when the result is sat; however, the displayed solutions might currently be difficult to read.

Note that only .smt2 files should be passed to Eldarica. The .c files under /heap-theory-examples/ are provided only for reference in order to show where the encodings came from, and should not be directly passed to Eldarica. This will result in an error as Eldarica does not have support for C programs with heap interactions (see TriCera for this, but note that it is also quite experimental at this point).

Eldarica 2.0.4

Various bugfixes. In addition, some new options to control CEGAR and predicate abstraction were added: -pPredicates: outputs all predicates computed by CEGAR, and -postHints: can read back those predicates (or other interpolation hints) in a later run. -noIntervals switches off the interval abstract domain, and interval constraint propagation.

Eldarica 2.0.3

This version mostly has changes in the underlying interpolation and decision procedure, Princess. In Eldarica itself, the handling of algebraic data-types has been improved, there is now an ADT pre-processor that should lead to problems with recursive data-types being solved more efficiently.