This talk will give a hands-on introduction to the software verification infrastructure consisting of the Horn solver Eldarica and the C model checker TriCera. After giving a high-level overview, the presenter will provide examples on how the tools can be used / extended for prototyping research ideas. Both tools are open-source and implemented in Scala.

Eldarica is a Horn solver that supports, among others, Horn clauses over the theories of integers, algebraic data-types, bit-vectors, arrays and the novel theory of heaps that simplifies encoding programs with heaps. Input clauses go through several preprocessing stages such as slicing, reachability analysis and inlining before being passed on to the main CEGAR engine that attempts to construct an abstract reachability graph that witnesses their satisfiability.

TriCera is a model checker for C programs that encodes input programs and specifications into a set of Horn clauses that can then be input to a Horn solver such as Eldarica or Z3/Spacer. TriCera mainly uses Eldarica for this purpose due to the tight integration of the tools and the theory of heaps. TriCera accepts most programs written in C11, and provides several other features useful for researchers: - the declaration and usage of uninterpreted predicates that can be seen as a form of inline assembler for Horn clauses, which simplify experimenting with various encodings, - automatic inference of loop invariants and function contracts, - parsing ACSL function contracts, - timing constraints in C programs (similar to UPPAAL timed automata), - concurrency.