Les méthodes formelles pour la conception des software et hardware génèrent souvent des formules qui doivent être validées, de manière interactive ou automatique. Parmi les outils automatiques, les solveurs SMT (Satisfiabilité Modulo Théories) sont particulièrement adaptés à la résolution de ces obligations de preuve, puisque leur langage d'entrée est la logique équationnelle avec des symboles provenant de divers fragments décidables utiles tels que les symboles non interprétés, l'arithmétique linéaire et des structures de données habituelles comme les tableaux ou les listes. Dans cette thèse, nous présentons une approche pour combiner des procédures de décision et des solveurs propositionnels dans un solveur SMT. Cette approche est fondée non seulement sur l'échange d'égalités déductibles entre les procédures de décision, mais aussi sur la génération d'égalités de modèle par des procédures de décision. Cela étend très bien la procédure classique de combinaison due à Nelson-Oppen dans une simple plate-forme pour combiner sans heurts des théories convexes et non convexes. Deuxièmement, nous présentons un algorithme original pour le fragment de l'arithmétique, appelé la logique de différence, et les détails sur la façon de mettre en oeuvre une procédure de décision basée sur cet algorithme. La logique de différence est modélisée en utilisant la théorie des graphes. Les déductions et les vérification de la cohérence effectués par l'algorithme se font par des recherches de cycles négatifs et des calculs de plus courts chemins de manière incrémentale. La dernière partie de la thèse présente une variation incrémentale originale de la méthode du simplexe que nous utilisons pour construire une procédure de décision pour l'arithmétique linéaire. Comme pour la logique de différence, nous présentons les détails de la procédure de décision qui la rend approprié pour notre plate-forme de combinaison utilisée par des solveurs SMT. Les méthodes et les techniques décrites dans cette thèse ont été mises en oeuvre et sont disponibles dans notre solveur SMT open-source, veriT.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00578254 |
| Date | 14 March 2011 |
| Creators | Caminha Barbosa De Oliveira, Diego |
| Publisher | Université Nancy II |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0019 seconds