CPBMC: a CP framework for Bounded Program Verification
The Constraint-Programming framework for Bounded Program Verification is a set of three tools that allow to automatically check properties of programs:
- CPBPV performs a depth-first traversal of a CFG (control flow graph).
- DPVS explores the CFG in a dynamic and non-sequential backward way.
- RAICP analyzes floating-point computations by combining abstract interpretation and constraint programming techniques.
FPCS: a floating point constraint solver
FPCS (Floating point constraint solver) is a floating point constraint solver, i.e., a solver with the capability to solve constraints extracted from a C program that does some computations over the floating point numbers.