English
CeV Contraintes et Vérification...

Logiciels

CPBMC: une plateforme pour la vérification de programmes basée sur la programmation par contraintes
Cette plateforme pour la vérification de programmes (model checking) basée sur la programmation par contraintes rassemble trois outils différents:
  • CPBPV adopte une approche "en profondeur" d'abord de parcours du graphe de flot de contrĂ´le
  • DPVS explore récursivement de manière dynamique et non séquentielle le graphe de flot de contrĂ´le
  • RAICP analyse les calculs sur les flottants en combinant interprétation abstrataite et programmation par contraintes
FPCS: un solveur de contraintes sur les flottants
FPCS (Floating point constraint solver) est un solveur de contraintes sur les flottants, i.e., un solveur capable de résoudre des contraintes issues d'un programme C effectuant des calculs sur les flottants selon la norme IEEE 754.
MCCS: un solveur d'optimisation multicrtères de problèmes de mise à jour de packages Linux
Le solveur MCCS (Multi Criteria CUDF Solver), développé dans le cadre du projet MANCOOSI, résout des problèmes d'optimisation de mise à jour de package Linux selon différents critères donnés par l'utilisateur.