A proof environment for concurrent programs
Identifieur interne : 00DB03 ( Main/Merge ); précédent : 00DB02; suivant : 00DB04A proof environment for concurrent programs
Auteurs : Naïma Brown [France] ; Dominique Méry [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
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:
DOI: 10.1007/BFb0024647
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
Links to Exploration step
ISTEX:E0073FC4A06832B1F02E47F3DE546EDCAD051904Le 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>
</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>
</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 00DB03 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00DB03 | 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é= ISTEX:E0073FC4A06832B1F02E47F3DE546EDCAD051904 |texte= A proof environment for concurrent programs }}
This area was generated with Dilib version V0.6.33. |