CeV Constraints and Verification ...


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.
MCCS: a multi criteria upgradeability optimization solver
The MCCS (Multi Criteria CUDF Solver) solver, which was devloped during the MANCOOSI project, solves multi criteria upgradeability problems described using the CUDF description language.