Le professeur Doron Peled, responsable du département d'informatique de l'Université Bar-Ilan, a récemment reçu un prix décerné lors de la 26ème conférence internationale CAV (Computer-Aided Verification) à Vienne. 

Ce prix récompense une carrière académique dont les travaux ont conduit à des avancées importantes pour les ordinateurs.

Une récompense prestigieuse

La conférence internationale CAV, organisée pour la première fois en 1986, est considérée comme l'une des plus prestigieuses en informatique théorique, et récompense chaque année des chercheurs ayant apporté une contribution majeure à ce domaine. 

Aux côtés du professeur Dolon Peled, trois autres scientifiques se sont vu remettre un prix cette année : les professeurs Antti Valmari, Pierre Wolper et Patrice Godefroid, travaillant respectivement à l'Université de technologies de Tampere en Finlande, à l'Université belge de Liège et au centre de recherche de Microsoft aux Etats-Unis. 

Cette célébration souligne plus particulièrement les travaux de ces quatre chercheurs dans le domaine de la vérification automatique de programmes.

Le bug de tous les dangers

L'informatique et le numérique ayant pris une part considérable dans notre société et plus particulièrement dans l'économie, le moindre bug peut avoir des conséquences désastreuses. 

Parmi les secteurs à haut risque, on peut citer la banque, la finance, l'énergie ou le transport. 

Et le risque d'un incident n'est pas nul, comme peut en témoigner le krach éclair intervenu à la bourse de New York courant 2010, causé par un bug dans un logiciel de trading automatique. 

Avec des conséquences malheureusement plus tragiques, un programme informatique défectueux fut également la source du dysfonctionnement du système de freinage de certains véhicules Toyota.

Si l'aléa existe, les entreprises essayent néanmoins, avec l'aide des chercheurs, de le réduire à son minimum. 

En matière informatique, différentes méthodes peuvent être utilisées pour réaliser une chasse aux bugs. 

La plus courante consiste à réaliser un audit du code en question par des experts, ces derniers étant alors chargés de repérer les portions d'un programme ayant une plus grande probabilité de voir apparaître des bugs.

Vérification formelle

Si cette dernière méthode est facile à mettre en place, elle est malheureusement loin d'être infaillible. 

Ainsi, pour des systèmes vraiment critiques telles que les transferts bancaires et l'informatique embarquée dans les avions et trains, on peut s'appuyer sur une autre pratique appelée vérification formelle de programme. 

Le principe consiste à faire analyser le code source du programme par une machine afin de vérifier qu'il respecte la spécification formelle décrivant son fonctionnement. 

De manière synthétique, il s'agit de fournir une preuve mathématique que le logiciel réalise le rôle qu'on lui assigne.

Le système chargé de la vérification conduit alors une exploration exhaustive de tous les scenarii possibles, et vérifie pour chacun d'entre eux que le programme se termine bien et donne le résultat escompté. 

Bien que la recherche dans le domaine, et plus particulièrement les travaux du professeur Doron Peled, ait justement permis de comprendre quels types de programmes pouvaient être ainsi analysés, on se rend compte intuitivement que la complexité d'une telle tâche ne permet pas de l'étendre à tous les systèmes en jeu. 

Industriels et chercheurs sont donc bien forcés de se concentrer sur les composantes critiques d'un logiciel.

Toujours est-il qu'au vu des enjeux considérables autour de ce domaine, le prix CAV ne risque pas d'être le chant du cygne du professeur Doron Peled !