Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00099468
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 9:14:44 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Friday, November 25, 2016 - 11:53:43 AM

Identifiers

  • 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⟩

Share

Metrics

Record views

95

Files downloads

66