Ongoing Projects

Program analysis and verification

• SLRP, Solver for Liveness of Randomised Parameterised systems
• Eldarica, a predicate abstraction-based model checker
• Eldarica-P, a model checker for Petri nets
• JayHorn, a model checker for Java applications
• The KeY project, deductive verification of Java applications

Theorem proving and SMT

• Princess, a theorem prover for Presburger arithmetic with uninterpreted predicates
• ePrincess, a theorem prover for first-order logic with equality, extending Princess with Bounded Rigid E-Unification (BREU)
• OSTRICH, a solver for string constraints with support for complex operations like replace-all and transduction
• Norn, a solver for string constraints, combining DPLL(T)-style reasoning with automata methods
• Sloth, a solver for string constraints based on a translation to alternating automata