# Ongoing Projects

#### Program analysis and verification

- SLRP,
Solver for Liveness of Randomised Parameterised systems
- Eldarica (now on
GitHub),
a predicate abstraction-based model checker
- Eldarica-P, a model checker for Petri nets
- Norn, a solver for string constraints
- JayHorn, a model checker for Java applications
- Bixie, a tool for detection of infeasible
code in Java applications
- The KeY project, deductive verification of Java applications

#### Theorem proving and arithmetic

- 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)