Combination methods for software verification = Méthodes de combinaison pour la vérification de logiciels

Divers
Université

Sous la direction de Italie) Università degli studi (Milan, Michaël Rusinowitch, Silvio Ghilardi, Silvio Ranise Thèse soutenue le 22 janvier 2008: Nancy 1 Cette thèse est consacrée au développement de méthodes formelles pour la vérification de logiciels. Parmi les techniques les plus utilisées dans ce contexte, il y en a deux qui permettent une spécification rigoureuse de toutes les exécutions possibles d'un système et le contrôle des bogues cachés. D'un côté, la correction d'un programme peut être garantie en démontrant l'insatisfiabilité d'une formule modulo une théorie qui axiomatise les types de données impliqués; de l'autre côté, les techniques de model-checking sont utilisées pour certifier que toute exécution possible du système satisfait les propriétés désirées. Les contributions de cette thèse sont les suivantes. Dans un premier temps, nous donnons un résultat de décidabilité pour la satisfiabilité de contraintes pour des extensions intéressantes de la théories des tableaux. Ensuite, nous avons obtenu des résultats dans le prolongement de Manna et Pnueli qui ont montré qu'un mélange de la logique du premier ordre et de la logique temporelle linéaire suffit pour énoncer les problèmes de vérification pour la classe des systèmes réactifs. Ainsi, nous nous inspirons de la récente littérature sur la combinaison des procédures de décision pour établir des résultats de décidabilité et d'indécidabilité pour le problème de satisfiabilité pour des logiques permettant d'intégrer du raisonnement modulo des théories du premier ordre dans un cadre temporel. Les résultats qu'on obtient pour la logiques temporelle linéaire sont ensuite généralisés au cas où le flux temporel est décrit par une logique dont le problème de la satisfiabilité relativisée est décidable. Notre dernière contribution est la décidabilité du problème du model-checking pour le flux temporel linéaire, sous des hypothèses appropriées concernant les théories du premier ordre impliquées. La preuve de ce r

Il n'y a aucune évaluation pour l'instant.


Soyez le premier à l'évaluer

Donnez votre évaluation
Combination methods for software verification = Méthodes de combinaison pour la vérification de logiciels
* Champs obligatoires
Votre commentaire
Vos notes
Clarté du contenu
Utilité du contenu
Qualité du contenu