Verification de logiciel C avec structures de memoire dynamiques – VERIDYC

Ce projet a pour but la verification des programmes C utilises pour le controle des systemes critiques, comme les centrales hydroelectriques ou nucleaires. L'enjeu majeur est le passage a l'echelle des techniques de verification existantes pour des programmes avec des structures de memoire dynamiques. Ces techniques sont capables de verifier de programmes sequentiels dont la taille ne depasse pas 100 lignes de code. Dans ce projet nous envisageons, d'une part l'extension des techniques existantes afin de pouvoir traiter les programmes parralleles avec des structures de liste et des tableaux, ainsi que, d'autre part, l'application de ces techniques a des etudes de cas reelles, dont la taille depassera 10K lignes de code. Le projet s'etalera sur deux axes de travail: 1. La generation des modeles a partir des programmes C parralleles. Il s'agit notamment de mettre en pratique des techniques de slicing et d'abstraction pour les programmes multithread, afin de garder les parties du code qui peuvent causer des erreurs comme les mauvaises manipulations de memoire, les blocages (dans le cas des programmes concurrents) ou les debordements des tableaux. 2. La verification, par rapport aux types d'erreurs mentionnes auparavant, a partir des modeles de taille raisonnable. Des techniques de verification ont ete developees pour les programmes mono-tache avec des structures de liste et des tableaux d'entiers. Il s'agit d'etendre ces techniques a de modeles multi-tache, en considerant les mecanismes de synchronisation par verrous, qui sont specifiques aux applications ecrites dans le langage C. Le resultat final du projet sera presente sous forme d'un outil prototype capable d'analyser un nombre d'etudes de cas fournis par les partenaires industriels (notamment EDF). 1. La generation des modeles a partir des programmes C parralleles. Il s'agit notamment de mettre en pratique des techniques de slicing et d'abstraction pour les programmes multithread, afin de garder les parties du code qui peuvent causer des erreurs comme les mauvaises manipulations de memoire, les blocages (dans le cas des programmes concurrents) ou les debordements des tableaux. 2. La verification, par rapport aux types d'erreurs mentionnes auparavant, a partir des modeles de taille raisonnable. Des techniques de verification ont ete developees pour les programmes mono-tache avec des structures de liste et des tableaux d'entiers. Il s'agit d'etendre ces techniques a de modeles multi-tache, en considerant les mecanismes de synchronisation par verrous, qui sont specifiques aux applications ecrites dans le langage C. Le resultat final du projet sera presente sous forme d'un outil prototype capable d'analyser un nombre d'etudes de cas fournis par les partenaires industriels (notamment EDF).