## Softwares

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.