Des logiciels plus fiables grâce aux démonstrations mathématiques
© 2015 Thinkstock
On peut tester les programmes informatiques à l’aide d’outils empruntés aux mathématiciens et à leurs fameuses démonstrations. Une équipe de l’EPFL ouvre une nouvelle voie dans ce domaine.
« Il faudrait changer les habitudes dans le marché du logiciel, juge Viktor Kuncak, professeur associé au Laboratoire d’analyse et de raisonnement automatisés de la Faculté Informatique et Communications. Les développeurs se reposent trop sur la possibilité de corriger les programmes après-coup, alors qu’ils sont déjà distribués sur le marché! » Pourtant, il existe des outils pour améliorer en amont la fiabilité de l’informatique. Ils sont d’ailleurs largement utilisés dans le domaine du développement hardware. « Lorsque l’on fabrique un microprocesseur, il n’est plus possible de le corriger une fois qu’il est produit. En fait, plus une erreur est découverte tard dans le processus de développement, plus elle coûtera cher. » Par ailleurs, un renforcement de la fiabilité des logiciels bénéficierait à divers domaines tels que l’aviation ou les appareils médicaux qui en deviendraient plus fiables.
Viktor Kuncak et le chercheur post-doc Andrew Reynolds travaillent au développement de tels outils de vérification automatique pour logiciels. Tout comme une démonstration mathématique cherche à montrer qu’une affirmation peut-être vraie pour un ensemble de valeurs, la validation informatique tend à s’assurer qu’une fonction ne provoquera pas de crash et ne retournera pas de valeur aberrante pour l’ensemble des saisies ou actions possibles pour l’utilisateur.
S’il est un outil auquel les mathématiciens ont régulièrement recours, c’est la démonstration par récurrence. Elle permet de démontrer la validité d’un théorème pour toute valeur entière. Elle consiste à prouver qu’un théorème est vrai pour toute valeur entière de n+1, en s’appuyant sur l’hypothèse qu’il est vrai pour n. Reste ensuite à prouver la validité du théorème pour la plus petite des valeurs : 0. Cette forme de démonstration n’était pas encore possible avec un solveur de contraintes complexes, appelé solveur SMT, satisfiability modulo theories, une des parties essentielles des outils de vérification automatique de logiciel. Cette barrière est désormais levée par les deux chercheurs de l’EPFL qui ont développé une approche permettant le recours automatique à l’induction mathématique (démonstration par récurrence) dans un processus de résolution de contraintes. Le langage d’entrée du code à vérifier est Scala, « nous l’avons choisi en raison de sa similarité avec les formulations et raisonnements mathématiques », explique Viktor Kuncak.
Outre l’informatisation de l’induction mathématique, cette approche se distingue aussi par une décomposition des tâches. « Lorsqu’une vérification ne peut être faite directement, notre outil décompose le problème en sous-problèmes qu’il sera peut-être à même de résoudre. Lorsqu’il existe un chemin connu alors il est utilisé, sinon d’autres pistes sont explorées et une nouvelle décomposition peut avoir lieu, permettant ainsi d’explorer un grand nombre de voies pour arriver à une résolution », décrit Viktor Kuncak.
Si les chercheurs de l’EPFL s’intéressent tout particulièrement à leurs applications en vérification de logiciels, les avancées apportées dans les domaines de l’automatisation des preuves mathématiques pourront bénéficier à d’autres domaines. « Le premier objectif des solveurs SMT était de résoudre divers problèmes rencontrés par l’industrie (la validation logicielle en fait partie). Plus récemment, on a commencé à les utiliser pour résoudre des problèmes plus complexes dont font partie les théorèmes mathématiques non démontrés (open mathematical problems). Jusqu’ici, cette application était relativement limitée, mais elle commence à être plus commune », explique Andrew Reynolds. « La liste de problèmes TPTP de l’Université de Miami est un projet qui va dans ce sens. L’utilisation de solveurs SMT tel que celui sur lequel je travaillais précédemment (CVC4) a permis de résoudre plusieurs de problèmes de cette liste. »
Les approches sur lesquels les chercheurs de l’EPFL travaillent s’avèrent intéressantes en termes de taux de succès et de vitesse d’exécution. Quelles sont les limites de cet outil ? « C’est un peu comme avec un élève doué, compare Viktor Kuncak, nous ne pouvons pas déterminer des limites théoriques, mais empiriquement nous constatons que certaines formules lui posent davantage de problèmes que d’autres. » Les recherches menées avec Andrew Reynolds à l’EPFL ont débuté en 2014. « Nous avons obtenu de bons résultats en seulement quelques mois, note Viktor Kuncak. L’EPFL a un certain leadership dans ce domaine que nous espérons pouvoir consolider».