InforLorV4, Main, Exploration, bibRecord, 00D230

A proof environment for concurrent programs

Identifieur interne : 00D230 ( Main/Exploration ); précédent : 00D229; suivant : 00D231

A proof environment for concurrent programs

Auteurs : Naïma Brown [France] ; Dominique Méry [France]

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:E0073FC4A06832B1F02E47F3DE546EDCAD051904

Abstract

Abstract: Unity [CM88, Mer92, Kna90], as action systems approach [BS91], is a formal method that attempts to decouple a program from its implementation. Therefore, Unity separates logical behaviour from implementation, it provides predicates for specifications, and proof rules for deriving specifications directly from the program text. This type of proof strategy is often clearer and more succinct than argument about a program's operational behaviour. Our research fits into Unity's methodology. Its aims to develop a proof environment suitable for mechanical proof of concurrent programs. This proof is based on Unity [CM88], and may be used to specify and verify both safety and liveness properties. Our verification method is based on theorem proving, so that an axiomatization of the operational semantics is needed. We use Dijkstra's wp-calculus to formalize the Unity logic, so we can always derive a sound relationship between the operational semantics of a given Unity specification and the axiomatic one from which theorems in our logic will be derived.

Url:

https://api.istex.fr/ark:/67375/HCB-92MV77TT-T/fulltext.pdf

DOI: 10.1007/BFb0024647

Affiliations:

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

to stream Istex, to step Corpus: 003539
to stream Istex, to step Curation: 003497
to stream Istex, to step Checkpoint: 002E77
to stream Main, to step Merge: 00DB03
to stream Main, to step Curation: 00D230

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A proof environment for concurrent programs</title>
<author><name sortKey="Brown, Naima" sort="Brown, Naima" uniqKey="Brown N" first="Naïma" last="Brown">Naïma Brown</name>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
<affiliation><country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:E0073FC4A06832B1F02E47F3DE546EDCAD051904</idno>
<date when="1993" year="1993">1993</date>
<idno type="doi">10.1007/BFb0024647</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-92MV77TT-T/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">003539</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003539</idno>
<idno type="wicri:Area/Istex/Curation">003497</idno>
<idno type="wicri:Area/Istex/Checkpoint">002E77</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002E77</idno>
<idno type="wicri:doubleKey">0302-9743:1993:Brown N:a:proof:environment</idno>
<idno type="wicri:Area/Main/Merge">00DB03</idno>
<idno type="wicri:Area/Main/Curation">00D230</idno>
<idno type="wicri:Area/Main/Exploration">00D230</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A proof environment for concurrent programs</title>
<author><name sortKey="Brown, Naima" sort="Brown, Naima" uniqKey="Brown N" first="Naïma" last="Brown">Naïma Brown</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>CRIN-CNRS & INRIA Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>CRIN-CNRS & INRIA Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<title level="s" type="abbrev">Lect Notes Comput Sci</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: Unity [CM88, Mer92, Kna90], as action systems approach [BS91], is a formal method that attempts to decouple a program from its implementation. Therefore, Unity separates logical behaviour from implementation, it provides predicates for specifications, and proof rules for deriving specifications directly from the program text. This type of proof strategy is often clearer and more succinct than argument about a program's operational behaviour. Our research fits into Unity's methodology. Its aims to develop a proof environment suitable for mechanical proof of concurrent programs. This proof is based on Unity [CM88], and may be used to specify and verify both safety and liveness properties. Our verification method is based on theorem proving, so that an axiomatization of the operational semantics is needed. We use Dijkstra's wp-calculus to formalize the Unity logic, so we can always derive a sound relationship between the operational semantics of a given Unity specification and the axiomatic one from which theorems in our logic will be derived.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Nancy</li>
<li>Vandœuvre-lès-Nancy</li>
</settlement>
<orgName><li>Centre national de la recherche scientifique</li>
<li>Institut national de recherche en informatique et en automatique</li>
<li>Laboratoire lorrain de recherche en informatique et ses applications</li>
<li>Mosel (Loria)</li>
<li>Université de Lorraine</li>
</orgName>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Brown, Naima" sort="Brown, Naima" uniqKey="Brown N" first="Naïma" last="Brown">Naïma Brown</name>
</region>
<name sortKey="Brown, Naima" sort="Brown, Naima" uniqKey="Brown N" first="Naïma" last="Brown">Naïma Brown</name>
<name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
<name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

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

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00D230 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00D230 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:E0073FC4A06832B1F02E47F3DE546EDCAD051904
   |texte=   A proof environment for concurrent programs
}}

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

A proof environment for concurrent programs

A proof environment for concurrent programs

Source :

Abstract

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

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

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