Eldarica - guide


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.

More information will be added shortly.

Contact Us| Privacy & Cookies | Terms of Use | Trademarks| © 2021 Microsoft