Completed or Past Projects

Program analysis and verification

• Joogie, a tool for detection of infeasible code in Java applications
• Bixie, a tool for detection of infeasible code in Java applications
• The KeYmaera project, deductive verification of hybrid systems
• Boogie, an intermediate verification language and analyser
• Rich Model Toolkit, COST initiative IC0901
  

Theorem proving and SMT

• 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

European projects on embedded systems and test-case generation

• CERTAINTY
  
• CESAR
• MOGENTES