Titre du sujet:

Vérification logicielle par analyse statique et méthodes symboliques

 

Encadrant:

Emmanuel Fleury et Jérôme Leroux

 

Directeur:

Igor Walukiewicz

 

Laboratoire et équipe de recherche:

LaBRI, équipe 'Méthode Formelle', thème 'Modélisation & Vérification'

 

Avec l'avènement de l'informatique embarquée et sa production en

masse la correction logicielle devient un enjeu crucial tant au niveau

humain dans les applications critiques qu'au niveau économique dans

les applications grand publique.

 

La vérification logicielle a pour sa part fait d'énormes

progrès depuis ses débuts. Il y a peu il était nécessaire

d'effectuer manuellement un travail de modélisation à partir du

programme original vers un formalisme particulier qui était

donné au vérificateur. De nos jours, les techniques

d'abstractions et les algorithmes d'exploration sur des domaines

abstraits nous permettent d'espérer prendre en entrée

directement un code source tel qu'il est compilé et d'en dériver

automatiquement un modèle puis de le vérifier. Évidemment,

l'expressivité des langages de programmation classiques (C, C++,

Java, ...) ne nous permettent pas d'espérer mieux que des

semi-algorithmes. Cependant, des outils tels que Blast, SLAM ou Magic

ont déjà montré qu'une telle chose était envisageable.

 

Le but de cette thèse est de combiner des techniques d'abstraction

venant de l'analyse statique et des algorithmes d'exploration d'espace

d'états venant du model-checking symbolique de systèmes infinis

afin de faire de la vérification de programmes à mémoire

dynamique et multi-threads.

 

Bibliographie:

 

[1] T. Ball and S. K. Rajamani. The SLAM Project: Debugging System

Software via Static Analysis, POPL 2002, January 2002, pages 1-3.

 

[2] T. Ball, R. Majumdar, T. Millstein and S. K. Rajamani. Automatic

Predicate Abstraction of C Programs, PLDI 2001, SIGPLAN Notices 36(5),

pp. 203-213.

 

[3] S. Bardin, A. Finkel, J. Leroux, P. Schnoebelen. Flat acceleration

in symbolic model checking. In Proc. 3rd Int. Symp. on Automated

Technology for Verification and Analysis (ATVA'05), Taipei, Taiwan,

Oct. 2005 , volume 3707 of Lecture Notes in Computer Science, pages

474-488. Springer, 2005.

 

[4] S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Fast

Acceleration of Symbolic Transition systems. In Proc. 15th

Int. Conf. Computer Aided Verification (CAV 2003), Boulder, CO, USA,

July 2003, volume 2725 of Lecture Notes in Computer Science, pages

118-121. Springer, 2003.

 

[5] P. Bouyer, F. Cassez, E. Fleury and K. G. Larsen. Optimal

Strategies in Priced Timed Game Automata. In Proceedings of the 24th

Conference on Fundations of Software Technology and Theoretical

Computer Science (FSTTCS'04), Chennai, India, December 2004, volume

3328 of Lecture Notes in Computer Science, pages 148-160. Springer.

 

[6] P. Bouyer, F. Cassez, E. Fleury and K. G. Larsen. Synthesis of

Optimal Strategies Using HyTech. In Proceedings of the Workshop on

Games in Design and Verification (GDV'04), Boston, Massachusetts, USA,

July 2004, ENTCS 119(1), pages 11-31. Elsevier Science Publishers,

2005.

 

[7] S. Chaki, E. Clarke, A. Groce, S. Jha and H. Veith. Modular

Verification of Software Components in C, Transactions on Software

Engineering (TSE), Volume 30, Number 6, pages 388-402, June 2004.

 

[8] S. Chaki, E. Clarke, A. Groce, S. Jha and H. Veith. Modular

Verification of Software Components in C, An ACM-SIGSOFT Distinguished

Paper in the 25th International Conference on Software Engineering

(ICSE) 2003, pages 385-395.

 

[9] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software

verification with BLAST. In Proc. 10th Int. SPIN Workshop (SPIN'2003),

Portland, OR, USA, May 2003, volume 2648 of Lecture Notes in Computer

Science, pages 235-239. Springer, 2003.