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.