Coopération de procédures de décision : étude et implantation
Identifieur interne : 005934 ( Hal/Corpus ); précédent : 005933; suivant : 005935Coopération de procédures de décision : étude et implantation
Auteurs : Duc-Khanh TranSource :
Descripteurs français
Abstract
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.
Url:
Links to Exploration step
Hal:inria-00099468Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr">Coopération de procédures de décision : étude et implantation</title><author><name sortKey="Tran, Duc Khanh" sort="Tran, Duc Khanh" uniqKey="Tran D" first="Duc-Khanh" last="Tran">Duc-Khanh Tran</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-2360" status="OLD"><idno type="RNSR">199221357D</idno><orgName>Constraints, automatic deduction and software properties proofs</orgName><orgName type="acronym">PROTHEO</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/protheo</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00099468</idno><idno type="halId">inria-00099468</idno><idno type="halUri">https://hal.inria.fr/inria-00099468</idno><idno type="url">https://hal.inria.fr/inria-00099468</idno><date when="2003">2003</date><idno type="wicri:Area/Hal/Corpus">005934</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Coopération de procédures de décision : étude et implantation</title><author><name sortKey="Tran, Duc Khanh" sort="Tran, Duc Khanh" uniqKey="Tran D" first="Duc-Khanh" last="Tran">Duc-Khanh Tran</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-2360" status="OLD"><idno type="RNSR">199221357D</idno><orgName>Constraints, automatic deduction and software properties proofs</orgName><orgName type="acronym">PROTHEO</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/protheo</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="fr"><term>combinaison</term><term>combination</term><term>decision procedures</term><term>procédures de décision</term><term>verification</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr">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.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="fr">Coopération de procédures de décision : étude et implantation</title><author role="aut"><persName><forename type="first">Duc-Khanh</forename><surname>Tran</surname></persName><email>Duc-Khanh.Tran@loria.fr</email><idno type="halauthor">130638</idno><orgName ref="#struct-364475"></orgName><affiliation ref="#struct-2360"></affiliation></author><editor role="depositor"><persName><forename>Publications</forename><surname>Loria</surname></persName><email>publications@loria.fr</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2006-09-26 09:14:44</date><date type="whenModified">2016-05-19 01:09:33</date><date type="whenReleased">2006-09-28 15:22:46</date><date type="whenProduced">2003</date><date type="whenEndEmbargoed">2015-02-10</date><ref type="file" target="https://hal.inria.fr/inria-00099468/document"><date notBefore="2015-02-10"></date></ref><ref type="file" n="1" target="https://hal.inria.fr/inria-00099468/file/A03-R-351.pdf"><date notBefore="2015-02-10"></date></ref></edition><respStmt><resp>contributor</resp><name key="108626"><persName><forename>Publications</forename><surname>Loria</surname></persName><email>publications@loria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">inria-00099468</idno><idno type="halUri">https://hal.inria.fr/inria-00099468</idno><idno type="halBibtex">tran:inria-00099468</idno><idno type="halRefHtml">[Stage] A03-R-351 || tran03a, 2003, 45 p</idno><idno type="halRef">[Stage] A03-R-351 || tran03a, 2003, 45 p</idno></publicationStmt><seriesStmt><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="INPL">Institut National Polytechnique de Lorraine</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LABO-LORIA-SET" p="LORIA">LABO-LORIA-SET</idno></seriesStmt><notesStmt><note type="commentary">Stage de DEA. || Le stage s'est fait en collaboration avec Silvio Ranise de l'équipe Cassis.. Rapport de stage.</note><note type="audience" n="0">Not set</note><note type="report" n="5">Intership report</note></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Coopération de procédures de décision : étude et implantation</title><author role="aut"><persName><forename type="first">Duc-Khanh</forename><surname>Tran</surname></persName><email>Duc-Khanh.Tran@loria.fr</email><idno type="halAuthorId">130638</idno><orgName ref="#struct-364475"></orgName><affiliation ref="#struct-2360"></affiliation></author></analytic><monogr><idno type="reportNumber">A03-R-351 || tran03a</idno><imprint><biblScope unit="pp">45 p</biblScope><date type="datePub">2003</date></imprint></monogr></biblStruct></sourceDesc><profileDesc><langUsage><language ident="fr">French</language></langUsage><textClass><keywords scheme="author"><term xml:lang="fr">combination</term><term xml:lang="fr">verification</term><term xml:lang="fr">decision procedures</term><term xml:lang="fr">procédures de décision</term><term xml:lang="fr">combinaison</term></keywords><classCode scheme="halDomain" n="info.info-oh">Computer Science [cs]/Other [cs.OH]</classCode><classCode scheme="halTypology" n="REPORT">Reports</classCode></textClass><abstract xml:lang="fr">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.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005934 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Corpus/biblio.hfd -nk 005934 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Corpus
|type= RBID
|clé= Hal:inria-00099468
|texte= Coopération de procédures de décision : étude et implantation
}}
| This area was generated with Dilib version V0.6.33. |  |