Coopération de procédures de décision : étude et implantation

Duc-Khanh Tran 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Les procédures de décision se trouvent au coeur de tous les outils modernes de l'analyse et la vérification des programmes car leur utilisation accroît d'une part l'efficacité du système de vérification et décharge d'autre part l'utilisateur de l'interaction, souvent fastidieuse, avec le système. Néanmoins, la plupart des problèmes de vérification font intervenir des mélanges de différentes théories par exemples les listes, les tableaux et les réels. Pour résoudre ce genre de problème il est fort souhaitable de procéder de façon modulaire en faisant coopérer les procédures de décision connues sur les théories élémentaires. Cette direction de recherche a été explorée pour la première fois il y a une vingtaine d'années grâce à des travaux précurseurs concernant la combinaison disjointe menés indépendamment par Shostak d'une part et Nelson-Oppen d'autre part dans le cadre de la vérification des programmes. Nos objectifs dans le cadre du stage concernent d'une part, la reformulation dans un cadre plus uniforme de la combinaison des deux approches Nelson-Oppen et Shostak et d'autre part, la proposition des nouvelles procédures de combinaisons dans différents contextes spécifiques, par exemple la combinaison des théories de Shostak et les théories stable-infinies. Nous abordons par la suite le problème de combinaison non-disjointe en présentant les travaux préliminaires menés par Ringeissen-Tinelli et par Zarba . Nous réalisons également une expérimentation dans le système de vérification haRVey développé au sein de l'équipe Cassis.
Type de document :
Rapport
[Stage] A03-R-351 || tran03a, 2003, 45 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00099468
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:14:44
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 11:53:43

Fichiers

Identifiants

  • HAL Id : inria-00099468, version 1

Collections

Citation

Duc-Khanh Tran. Coopération de procédures de décision : étude et implantation. [Stage] A03-R-351 || tran03a, 2003, 45 p. 〈inria-00099468〉

Partager

Métriques

Consultations de la notice

60

Téléchargements de fichiers

29