Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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ésultat indique qu'on pourrait employer avec succès des Solveurs Modulo des Théories dans les applications du model-checking aux systèmes ayant un nombre infini d'états. ; The thesis is devoted to the ...