Vérification automatisée de systèmes logiciels – AVERISS

La vérification de programmes est une tˆache difficile qui repr´esente un th`eme de recherche important. L'objectif
de ce projet est de fournir des techniques avanc´ees pour la v´erification automatique du logiciel, en
prenant compte des aspects complexes de tels syst`emes ´ecrits dans des langages de programmation usuels
(tels que C ou Java). Parmi ces aspects, citons : la manipulation de donn´ees, les appels de proc´edures, la
param´etrisation, la cr´eation de processus, la concurrence, l'inclusion de code externe, etc.
Notre approche est bas´ee sur une combinaison ´etroite de (1) techniques d'abstraction appliquable directement
au code source du programme permettant d'extraire automatiquement des mod`eles pr´ecis bas´es
sur les automates, mais pouvant ˆetre en g´en´eral des syst`emes ayant un nombre infini d'´etats, et (2) des
techniques algorithmiques pour l'analyse (exacte/approch´ee) de ces mod`eles expressifs. Les abstractions
appliqu´ees sont d´efinies automatiquement et raffinable au besoin en utilisant le r´esultat de l'analyse. Les
techniques d'analyse sont bas´ees sur le model-checking symbolique pour syst`emes infinis, utilsant des
repr´esentations finies (bas´ees sur les automates/logique) d'ensemble infinis de configurations.
Nous comptons d´evelopper de telles m´ethodes algorithmiques pour aussi bien la v´erification des propri´et´es
de sˆuret´e que pour la v´erification de la terminaison des programmes. De plus, nous allons consid´erer ces
probl`emes de v´erification aussi bien pour les syst`emes ferm´es (dont tous les composants sont compl´etement
d´efinis) que pour les syst`emes ouverts dont certains des composants ne sont que partiellement sp´ecifi´es
(par exemple dans le cas de programmes invoquant du code externe).
Les m´ethodes et techniques d´evelopp´ees dans le projet seront impl´ement´ees dans de nouveaux outils
de v´erification, et exp´eriment´es sur des probl`emes de v´erification non triviaux concernant des syst`emes
logiciels de taille r´eelle (tels que des noyaux de syst`emes d'expoitation, ou des serveurs web).