AbSolute : AbSolute

Équipe : APR

AbSolute est un solveur de contraintes basé sur les domaines abstraits. Il implémente la méthode de résolution présenté dans l'article : Marie Pelleau, Antoine Miné, Charlotte Truchet, Frédéric Benhamou, Constraint Solver based on Abstract Domains, 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Rome, Italie, 2013 [Article] Ce solveur peut résoudre des problèmes continus, discrets et mixtes (contenant des variables entières et réelles) et propose des techniques permettant de traiter aussi bien les contraintes linéaires que non-linéaires. La méthode de résolution prend en compte les erreurs d'arrondi et calcule des approximations flottantes sures des solutions réelles d'un problème. AbSolute utilise Apron, une librairie Ocaml de domaines abstraits, qui permet de résoudre des problèmes à l'aide d'autre domaines abstraits que les intervalles.

Responsable : Marie PELLEAU
https://github.com/mpelleau/AbSolute