Projects (in which I am or have been involved)

Deduction and program verification

• The KeY project
• The KeYmaera project
• The Boogie verifier
• Rich Model Toolkit
  

Reasoning in Presburger arithmetic

• Princess, a theorem prover for Presburger arithmetic with uninterpreted predicates
• iPrincess, a theorem prover based on Princess that can compute Craig interpolants for quantifier-free Presburger arithmetic with uninterpreted predicates
• Seneschal, a ranking function generator for Presburger arithmetic and machine arithmetic

Satisfiability Modulo Theories (SMT)

• Theories of finite lists, sets, and maps for the SMT-LIB standard
  

European projects on embedded software and test-case generation

• CESAR
• MOGENTES