Projet ANR-13-IS02-0001 – SMArT : Satisfaisabilité Modulo Arithmétique et Théories
Programme : Blanc – Accords bilatéraux 2013 - SIMI 2 - Science informatique et applications (Blanc – Accords bilatéraux 2013 - SIMI 2) 2013
Année de financement : 2013
Coordinateur du projet : Monsieur Pascal FONTAINE (Laboratoire Lorrain de Recherche en Informatique et ses Applications)
Partenaires : Laboratoire Lorrain de Recherche en Informatique et ses Applications; MPI-INF Max Planck Institut Informatik; SYSTEREL
Montant : 125249.0 euros
Date de début : 2014
Durée : 42 mois
Résumé : Le projet vise à combler le fossé entre les techniques modernes de raisonnement automatique sur l'arithmétique et la vérification formelle.  Depuis une décennie, la vérification symbolique connaît des progrès considérables, dus en particulier au développement des techniques et solveurs SMT (satisfaisabilité modulo théorie).  Ces solveurs sont utilisés avec succès notamment pour la vérification de programmes, le model-checking borné ou paramétré et la génération de test.  Ils allient la puissance d'un solveur SAT pour décider la satisfaisabilité de la logique propositionnelle, avec des raisonneurs de théorie pour décider la satisfaisabilité d'ensembles de littéraux sur des symboles interprétés, les quantificateurs étant gérés par des techniques d'instantiation.
Les tâches de vérification nécessitent souvent de raisonner dans des fragments arithmétiques.  Ici nous comprenons "arithmétique" dans un sens large, comprenant toute théorie interprétant constantes et fonctions (0, 1, +, *, et aussi mod, div, exp, fonctions trigonométriques,...) sur les entiers, rationnels, réels, ou complexes, ou même plusieurs de ces domaines.  Pour obtenir la décidabilité, il est nécessaire de restreindre fortement le langage, et les fragments décidables ont parfois une complexité prohibitive.  En pratique cependant, les problèmes s'expriment souvent dans des sous-fragments simples de l'arithmétique.
Les SMT solveurs actuels sont essentiellement limités aux formules sans quantificateurs avec arithmétique linéaire (les seuls symboles arithmétiques autorisés sont les constantes, +, et 
Notre approche est d'adapter les techniques et algorithmes efficaces existants, en s'appuyant sur les outils disponibles, de façon à ce qu'ils puissent être utilisés dans un contexte SMT.  Les avantages de cette approche sont: (1) l'outil arithmétique ne doit pas gérer la structure Booléenne, (2) l'infrastructure (structures de données et algorithmes) évoluée qui permet de gérer les fragments arithmétiques expressifs est disponible dans le solveur SMT, (3) l'utilisateur bénéficie de l'architecture modulaire des solveurs SMT, où l'arithmétique peut être combinée avec d'autres théories d'intérêt.
Cette approche d'intégration nécessite un travail fondamental sur les procédures de (semi-)décision arithmétiques: génération de modèles, de coeurs insatisfaisables, calcul d'égalités impliquées,etc.  Parallèlement, l'intégration efficace de l'arithmétique non linéaire dans un solveur SMT nécessite de relaxer un certain nombre d'exigences des solveurs SMT: entre autre, la théorie n'est pas convexe, ni disjointe de l'arithmétique linéaire.
À côté des contributions fondamentales, nos techniques seront implémentées dans un solveur intégrant Redlog, un solveur efficace de référence pour l'arithmétique non linéaire, et veriT, un solveur SMT moderne.  Cette intégration sera diffusée en open-source sous une licence permissive (comme nos outils le sont actuellement), pour que la communauté scientifique en bénéficie et puisse intégrer et améliorer cette intégration dans les autres plates-formes de vérification.  Nous évaluerons quantitativement nos résultats en appliquant le solveur à des problèmes issus de librairie de problèmes SMT-LIB et des plates-formes de vérification Rodin et TLAPS.  Le consortium inclut des développeurs principaux de ces deux plates-formes de vérification.