InforLorV4, Main, Merge, bibRecord, 008D47

Using automated induction-based theorem provers for reasoning about concurrent systems

Identifieur interne : 008D47 ( Main/Merge ); précédent : 008D46; suivant : 008D48

Using automated induction-based theorem provers for reasoning about concurrent systems

Auteurs : Abdessamad Imine [Tunisie] ; Yahya Slimani [Tunisie] ; Sorin Stratulat [France]

Source :

RBID : Pascal:02-0579723

Descripteurs français

Pascal (Inist)
- Induction, Démonstration théorème, Simultanéité informatique, Système expert, Logique temporelle, Exclusion mutuelle, Récurrence, Sémantique, Spécification, Démonstration automatique.

English descriptors

KwdEn :
- Automatic proving, Concurrency, Expert system, Induction, Mutual exclusion, Recurrence, Semantics, Specification, Temporal logic, Theorem proving.

Abstract

Nous proposons une combinaison de logique temporelle et du raisonnement inductif afin de spécifier et de vérifier des systèmes concurrents. Plus précisément, nous décrivons un essai d'automatiser le raisonnement sur des systèmes concurrents, décrits par des spécifications TLA (Temporal Logic of Actions). SPIKE, un démonstrateur automatique de théorèmes basé sur la récurrence, est utilisé pour formaliser la sémantique de TLA, puis de raisonner sur des algorithmes spécifiés en TLA. Comme étude de cas, nous illustrons une preuve d'invariance pour un algorithme d'exclusion mutuelle.

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000847
to stream PascalFrancis, to step Curation: 000205
to stream PascalFrancis, to step Checkpoint: 000762

Links to Exploration step

Pascal:02-0579723

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Using automated induction-based theorem provers for reasoning about concurrent systems</title>
<author><name sortKey="Imine, Abdessamad" sort="Imine, Abdessamad" uniqKey="Imine A" first="Abdessamad" last="Imine">Abdessamad Imine</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA, INRIA, Campus Scientifique B.P. 239</s1>
<s2>54506 Vandeouvre-les-Nancy</s2>
<s3>TUN</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>Tunisie</country>
<wicri:noRegion>54506 Vandeouvre-les-Nancy</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Slimani, Yahya" sort="Slimani, Yahya" uniqKey="Slimani Y" first="Yahya" last="Slimani">Yahya Slimani</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Dépt. Informatique - Faculté des Sciences de Tunis, Campus Universitaire </s1>
<s2>1060 Tunis</s2>
<s3>TUN</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Tunisie</country>
<placeName><settlement type="city">Tunis</settlement>
<region nuts="2">Gouvernorat de Tunis</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Stratulat, Sorin" sort="Stratulat, Sorin" uniqKey="Stratulat S" first="Sorin" last="Stratulat">Sorin Stratulat</name>
<affiliation wicri:level="3"><inist:fA14 i1="03"><s1>INRIA, 2004, mute des Lucioles - BP 93</s1>
<s2>06902 Sophia Antipolis</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Provence-Alpes-Côte d'Azur</region>
<settlement type="city">Sophia Antipolis</settlement>
</placeName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">02-0579723</idno>
<date when="2002">2002</date>
<idno type="stanalyst">PASCAL 02-0579723 INIST</idno>
<idno type="RBID">Pascal:02-0579723</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000847</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000205</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000762</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000762</idno>
<idno type="wicri:Area/Main/Merge">008D47</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Using automated induction-based theorem provers for reasoning about concurrent systems</title>
<author><name sortKey="Imine, Abdessamad" sort="Imine, Abdessamad" uniqKey="Imine A" first="Abdessamad" last="Imine">Abdessamad Imine</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA, INRIA, Campus Scientifique B.P. 239</s1>
<s2>54506 Vandeouvre-les-Nancy</s2>
<s3>TUN</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>Tunisie</country>
<wicri:noRegion>54506 Vandeouvre-les-Nancy</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Slimani, Yahya" sort="Slimani, Yahya" uniqKey="Slimani Y" first="Yahya" last="Slimani">Yahya Slimani</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Dépt. Informatique - Faculté des Sciences de Tunis, Campus Universitaire </s1>
<s2>1060 Tunis</s2>
<s3>TUN</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Tunisie</country>
<placeName><settlement type="city">Tunis</settlement>
<region nuts="2">Gouvernorat de Tunis</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Stratulat, Sorin" sort="Stratulat, Sorin" uniqKey="Stratulat S" first="Sorin" last="Stratulat">Sorin Stratulat</name>
<affiliation wicri:level="3"><inist:fA14 i1="03"><s1>INRIA, 2004, mute des Lucioles - BP 93</s1>
<s2>06902 Sophia Antipolis</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Provence-Alpes-Côte d'Azur</region>
<settlement type="city">Sophia Antipolis</settlement>
</placeName>
</affiliation>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Automatic proving</term>
<term>Concurrency</term>
<term>Expert system</term>
<term>Induction</term>
<term>Mutual exclusion</term>
<term>Recurrence</term>
<term>Semantics</term>
<term>Specification</term>
<term>Temporal logic</term>
<term>Theorem proving</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Induction</term>
<term>Démonstration théorème</term>
<term>Simultanéité informatique</term>
<term>Système expert</term>
<term>Logique temporelle</term>
<term>Exclusion mutuelle</term>
<term>Récurrence</term>
<term>Sémantique</term>
<term>Spécification</term>
<term>Démonstration automatique</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="fr">Nous proposons une combinaison de logique temporelle et du raisonnement inductif afin de spécifier et de vérifier des systèmes concurrents. Plus précisément, nous décrivons un essai d'automatiser le raisonnement sur des systèmes concurrents, décrits par des spécifications TLA (Temporal Logic of Actions). SPIKE, un démonstrateur automatique de théorèmes basé sur la récurrence, est utilisé pour formaliser la sémantique de TLA, puis de raisonner sur des algorithmes spécifiés en TLA. Comme étude de cas, nous illustrons une preuve d'invariance pour un algorithme d'exclusion mutuelle.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>Tunisie</li>
</country>
<region><li>Gouvernorat de Tunis</li>
<li>Provence-Alpes-Côte d'Azur</li>
</region>
<settlement><li>Sophia Antipolis</li>
<li>Tunis</li>
</settlement>
</list>
<tree><country name="Tunisie"><noRegion><name sortKey="Imine, Abdessamad" sort="Imine, Abdessamad" uniqKey="Imine A" first="Abdessamad" last="Imine">Abdessamad Imine</name>
</noRegion>
<name sortKey="Slimani, Yahya" sort="Slimani, Yahya" uniqKey="Slimani Y" first="Yahya" last="Slimani">Yahya Slimani</name>
</country>
<country name="France"><region name="Provence-Alpes-Côte d'Azur"><name sortKey="Stratulat, Sorin" sort="Stratulat, Sorin" uniqKey="Stratulat S" first="Sorin" last="Stratulat">Sorin Stratulat</name>
</region>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 008D47 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 008D47 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Merge
   |type=    RBID
   |clé=     Pascal:02-0579723
   |texte=   Using automated induction-based theorem provers for reasoning about concurrent systems
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Using automated induction-based theorem provers for reasoning about concurrent systems

Using automated induction-based theorem provers for reasoning about concurrent systems

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri