ASTRÉE, le débugger automatique

J’ai découvert il y a quelques jours le projet d’un groupe de chercheurs à l’ÉNS, qui conçoivent un analyseur de code source détectant les bugs à l’exécution (ceux que le compilateur le signale pas, c’est à dire les erreurs de segmentation, les débordements d’entiers, les pertes de précision en calcul flottant, la division par zéro, etc). C’est assez passionnant (normal, c’est de la sémantique). Le principe — si j’ai bien compris — est d’associer à chaque variable un intervale de valeurs possibles à un état donné et de détecter comme ça les états critiques. Le logiciel est conçu pour toujours sur-estimer le risque, et donc s’il ne renvoie aucune erreur, la preuve est faite que le logiciel ne peut pas rencontrer ce type de bugs. La validité des résultats donnés en sortie par le logiciel n’est pas du tout prise en compte, c’est juste l’absence de certains bugs qui sont garantis.

Une vidéo d’une demie heure présente le système (c’est une conférence très didactique, pas uniquement compréhensible par des chercheurs). Domage que le logiciel ne soit accessible qu’aux entreprises et que les concepteurs ne donnent pas plus d’informations sur son fonctionnement interne (une distribution sous licence libre semble inimaginable).

Je ne sais pas si ça existe et si c’est techniquement abordable, mais je trouve que ça donne envie d’écrire d’autres analyseurs de code source, à d’autres fins, par exemple pour estimer la complexité spatiale ou temporelle d’une fonction. L’approche naïve serait de compter le nombre de boucles imbriquées, puis de « comprendre » un peu plus le fonctionnement de l’algorithme. Ça existe peut-être déjà.