# 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