AbSolute : AbSolute

Team : APR

AbSolute is a constraint solver based on abstract domains. It implements the resolution method presented in the article: (VMCAI), Rome, Italy, 2013 [Article] [Article in French] Antoine Miné, Charlotte Truchet, Frédéric Benhamou, Constraint Solver based on Abstract Domains, 14th International Conference on Verification, This solver can solve continuous, discrete and mixed problems (containing both integer and real variables) and proposes techniques for processing both linear and non-linear constraints. Rounding errors are taken into account during the resolution. The solver calculates sound float approximations of the real solutions of a problem. AbSolute uses Apron, an Ocaml library of abstract domains, which solves problems using other abstract domains than intervals.

Software leader : Marie PELLEAU