DIXIT : a Graphical Toolkit for Predicate Abstractions
Identifieur interne : 005F61 ( Main/Curation ); précédent : 005F60; suivant : 005F62DIXIT : a Graphical Toolkit for Predicate Abstractions
Auteurs : Loïc Fejoz ; Dominique Méry [France] ; Stephan MerzSource :
English descriptors
Abstract
We describe a toolkit to support the use of predicate diagrams, a representation of predicate abstractions that includes annotations for proving liveness properties. Centered around a graphical editor for drawing predicate diagrams, proof obligations for proving correctness of the abstraction w.r.t. TLA+ system specifications can be generated, correctness properties expressed in temporal logic can be verified by model checking, and counterexamples can be visualized. The toolkit also supports stepwise development of systems, based on a notion of refinement of predicate diagrams.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: Pour aller vers cette notice dans l'étape Curation :004417
- to stream Crin, to step Curation: Pour aller vers cette notice dans l'étape Curation :004417
- to stream Crin, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :000409
- to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :006184
Links to Exploration step
CRIN:fejoz05aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="257">DIXIT : a Graphical Toolkit for Predicate Abstractions</title></titleStmt><publicationStmt><idno type="RBID">CRIN:fejoz05a</idno><date when="2005" year="2005">2005</date><idno type="wicri:Area/Crin/Corpus">004417</idno><idno type="wicri:Area/Crin/Curation">004417</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">004417</idno><idno type="wicri:Area/Crin/Checkpoint">000409</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000409</idno><idno type="wicri:Area/Main/Merge">006184</idno><idno type="wicri:Area/Main/Curation">005F61</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">DIXIT : a Graphical Toolkit for Predicate Abstractions</title><author><name sortKey="Fejoz, Loic" sort="Fejoz, Loic" uniqKey="Fejoz L" first="Loïc" last="Fejoz">Loïc Fejoz</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><author><name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>liveness properties</term><term>model checking</term><term>predicate abstraction</term><term>theorem proving</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="1566">We describe a toolkit to support the use of predicate diagrams, a representation of predicate abstractions that includes annotations for proving liveness properties. Centered around a graphical editor for drawing predicate diagrams, proof obligations for proving correctness of the abstraction w.r.t. TLA+ system specifications can be generated, correctness properties expressed in temporal logic can be verified by model checking, and counterexamples can be visualized. The toolkit also supports stepwise development of systems, based on a notion of refinement of predicate diagrams.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005F61 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 005F61 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Curation
|type= RBID
|clé= CRIN:fejoz05a
|texte= DIXIT : a Graphical Toolkit for Predicate Abstractions
}}
| This area was generated with Dilib version V0.6.33. |  |