I have developed several tools in the course of my work. Please contact me if you need help with them.

  • SeaHorn, a software verification framework
  • Avy, a hardware model checker
  • Spacer, an SMT Horn Clause solver
  • FrankenBit, a bit-precise software verifier
  • UFO, a software verification framework
  • Rek, a Bounded Model Checker for Real-Time Embedded Systems
  • LDD/BOXES, a Linear Decision Diagram package and BOXES abstract domain
  • Yasm, a Software Model Checker based on Predicate Abstraction and Belnap logic
  • VaqUoT, a vacuity detector for NuSMV
  • XChek, a multi-valued Model Checker