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