All of these tools were realized with significant contributions by various colleagues and in particular by Ph.D. students
  • FunFrog - Function-summarization-based Bounded ModelChecker
  • eVolCheck - Interpolation-based Upgrade Checker
  • LoopFrog - Abstract Interpretation-based static analyzer
  • OpenSMT - Open source SMT solver
  • Periplo - Open source SAT solver, proof transformation and interpolation engine
  • SAFARI - Model checker for programs with arrays
  • SATABS - Model checker for C programs
  • ComFoRT - Formal reasoning framework for analysis of component-based designs
  • ObjectCheck - Toolset for Design and Analysis of Object-Oriented Programs