recherche
vérification automatique
05/12/2010
Introduction
La conception de programmes corrects a toujours été considérée comme une tâche complexe. Tout un chacun a expérimenté le temps nécessaire à l'élimination des erreurs non intentionnelles de programmation, les bugs, souvent bien plus important que le temps dispensé dans l'écriture du programme même.
L'utilisation des logiciels informatiques se généralise et l'on est de plus en plus dépendant de leur fiabilité. Les conséquences d'un comportement anormal peuvent être dramatiques, soit en terme de pertes financières, comme ce fut le cas par exemple pour le crash en 1996 de l'Ariane 5, soit en terme de vies humaines dans le cas de systèmes critiques (pilotage des centrales nucléaires, logiciels pour l'aéronautique, ...).
Si l'industrie du logiciel a pris conscience de la nécessité d'assurer la correction des programmes après leur conception, il s'avère que la complexité des logiciels semble suivre la loi de Moore et que de nombreux aspects complexes tels que la manipulation de structures de données non bornées, la concurrence, les processus parallèles, etc compliquent à l'extrême la validation du logiciel.
La vérification est une classe de techniques de validation, basée sur des méthodes formelles permettant de prouver qu'un système est conforme à ses spécifications quelle que soit la situation à laquelle il est soumis, à la différence des techniques de test.
domaine numérique abstrait et propriétés d'égalité / non-égalité
- stage de master
- laboratoire VERIMAG sous la direction de Nicolas Halbwachs
- juin 2005 - transparents:
-
IS, un domaine numérique abstrait pour l'analyse de programmes manipulant des adresses
@mastersthesis{,
author = {Mathias Péron},
title = {IS, un domaine numérique abstrait pour l'analyse de programmes manipulant des adresses},
year = {2005},
school = {VERIMAG},
url={http://perso.ens-lyon.fr/mathias.peron/}
}
Bibliographie
Les références au format bibtex que j'ai utilisé sur ce thème.