CeV (Contraintes et Vérification) rassemble des compétences allant de la programmation par contraintes à la vérification de programmes. CeV explore les capacités des techniques de programmation par contraintes dans le cadre de la vérification de programmes, une des problématiques des plus critiques lors du développement du logiciel. Récemment, les techniques de programmation par contraintes ont été appliquées avec succès à plusieurs domaines de la vérification, allant de la génération automatique de cas de tests à la détection automatique de non conformités d'un programme vis à vis de sa spécification. C'est dans ce cadre que CeV s'intéresse principalement aux thèmes suivants:

• Détection automatique de non conformités d'un programme vis à vis de sa spécification: Lorsque qu'un programme est "borné", que ce soit par sa structure ou par grâce à des informations fournies par l'utilisateur, la programmation par contraintes peut alors être utilisée afin de détecter automatiquement des cas de non conformités du programme vis à vis de sa spécification. Le programme est d'abord mis sous forme relationnelle et combiné avec une négation de sa spécification. Un solveur est alors utilisé pour obtenir des solutions à ce problème de contraintes, chacune d'entre elles constituant un contre exemple montrant une non conformité entre le programme et sa spécification. Le défi consiste à construire un processus de résolution efficace et adapté à la vérification.
   
• La combinaison des techniques d'interprétation abstraite et de programmation par contraintes: L'interprétation abstraite et la programmation par contraintes sont deux techniques caractérisées par leur capacité à déterminer les domaines de valeurs des variables d'un programme. Alors que la première se montre capable de traiter des programmes de taille conséquente, la seconde peine à passer à l'échelle. Et si la programmation par contrainte permet souvent de déterminer avec précision les domaines de valeurs, l'interprétation abstraite en fourni parfois des approximations trop laches. Rapprocher ces deux techniques dans le cadre de la vérification devrait permettre de combiner leur forces et de pallier leur faiblesses respectives.
   
• L'aide à la localisation d'erreurs: L'utilisation de la programmation par contraintes pour la détection automatique de non conformités d'un programme vis à vis de sa spécification permet de générer des contre exemples qui devraient aider l'utilisateur à comprendre les erreurs contenues dans le programme. Cependant, ces contre exemples ne fournissent pas directement l'emplacement de l'erreur. La programmation par contraintes peut être utiliser pour aider l'utilisateur à déterminer l'emplacement de l'erreur en calculant le sous ensemble du programme qui ne contredit pas le contre exemple et la spécification. Le problème est alors de calculer les sous ensembles les plus pertinents et de fournir des explication plausibles de l'erreur.
   
• Les contraintes sur les flottants: L'analyse de programmes utilisant des calculs sur les flottants, dont l'usage ne cesse de croître, nécessite des contraintes spécifiques capables de prendre en compte les particularités de l'arithmétique sur les flottants. Cette dernière ne peut être correctement capturée par des solveurs sur les réels, solveurs qui ne sont pas conservatif de l'ensemble des solutions sur les flottants. Le développement de solveurs dédiés aux flottants est donc nécessaire pour une analyse correcte de ces programmes.
   

CeV fait partie de l'équipe MDSC de l'I3S, une unité mixte de recherches commune à l'université de Nice et au CNRS.