Beaucoup d'applications des méthodes formelles reposent sur la génération de formules en logique du premier ordre et la preuve de leur satisfiabilité par rapport à une théorie en arrière-plan, qui est souvent obtenu par mélange de plusieurs théories. Dans la littérature, cette forme de satisfiabilité est appelée Satisfiabilité Modulo Théories (SMT). Dans cette thèse, on s'intéresse à la conception de procédures de décision pour les problèmes SMT, en intégrant des techniques de saturation basées sur la réécriture pour des théories finiment axiomatisées et des techniques de combinaison pour des unions de théories. La première contribution de cette thèse est une reconstruction raisonnée, dans un cadre uniforme, des méthodes de combinaison proposées par Nelson-Oppen, Shostak et d'autres. Ceci est le point de départ pour de nouvelles investigations. Nous introduisons ensuite le concept de canoniseur étendu et dérivons un résultat de modularité pour une nouvelle classe de théories, ce qui contraste avec l'absence de modularité pour la classe de théories considérée par Shostak. La deuxième contribution concerne le problème de la combinaison de procédures basées sur la réécriture en utilisant la méthode de Nelson-Oppen. Nous utilisons la méta-saturation pour développer des techniques de preuve automatique permettant de tester les conditions pour la combinabilité de telles procédures. Lorsque la méta-saturation termine pour une théorie, le résultat obtenu permet de raisonner sur la combinabilité pour cette théorie d'une procédure de satisfiabilité basée sur la réécriture. La troisième contribution de cette thèse est liée à l'intégration des procédures de décision dans les solveurs SMT. Nous considérons le problème de rajouter aux procédures de décision la capacité de construire des justifications en cas d'insatisfiabilité, sans dégradation des performances, en nous focalisant sur la construction modulaire de telles justifications pour une théorie combinée. Pour ce faire, nous étendons la méthode de combinaison de Nelson-Oppen de manière à construire de façon modulaire des justisfications d'insatisfiabilité pour des unions de théories. Nous étudions également comment les justifications obtenues peuvent être reliées à une forme appropriée de minimalité.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00580582 |
| Date | 16 February 2007 |
| Creators | Tran, Duc-Khanh |
| Publisher | Université Henri Poincaré - Nancy I |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0026 seconds