DIXIT : a Graphical Toolkit for Predicate Abstractions
Identifieur interne : 004417 ( Crin/Curation ); précédent : 004416; suivant : 004418DIXIT : a Graphical Toolkit for Predicate Abstractions
Auteurs : Loïc Fejoz ; Dominique Mery ; 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
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></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 Mery</name></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><BibTex type="inproceedings"><ref>fejoz05a</ref><crinnumber>A05-R-407</crinnumber><category>3</category><equipe>MOSEL</equipe><author><e>Fejoz, Loïc</e><e>Mery, Dominique</e><e>Merz, Stephan</e></author><title>DIXIT : a Graphical Toolkit for Predicate Abstractions</title><booktitle>{Fourth International Workshop on Automated Verification of Infinite-State Systems - AVIS'05, Edinburgh, UK}</booktitle><year>2005</year><editor>Ramesh Bharadwaj and Supratik Mukhopadhyay</editor><pages>39--48</pages><month>apr</month><keywords><e>predicate abstraction</e><e>model checking</e><e>theorem proving</e><e>liveness properties</e></keywords><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.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004417 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Curation/biblio.hfd -nk 004417 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|é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. |  |