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.