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 is a constraint solver over floating-point numbers based on improvements in the computation of the bounds of the inverse projection functions of arithmetic operations.
MCCS: a Multi Criteria CUDF Solver
mccs take as input a CUDF problem and computes the best solution according to a set of criteria.