Context-Switch-Directed Verification in DIVINE

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00084599" target="_blank" >RIV/00216224:14330/14:00084599 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-14896-0_12" target="_blank" >http://dx.doi.org/10.1007/978-3-319-14896-0_12</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-14896-0_12" target="_blank" >10.1007/978-3-319-14896-0_12</a>

Result language
angličtina
Original language name
Context-Switch-Directed Verification in DIVINE
Original language description
In model checking of real-life C and C++ programs, both search efficiency and counterexample readability are very important. In this paper, we suggest context-switch-directed exploration as a way to find a well-readable counterexample faster. Furthermore, we allow to limit the number of context switches used in state-space exploration if desired. The new algorithm is implemented in the DIVINE model checker and enables both unbounded and bounded context-switch-directed exploration for models given in LLVM bitcode, which efficiently allows for verification of multi-threaded C and C++ programs.
Czech name
—
Czech description
—

Publication year
2014
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Mathematical and Engineering Methods in Computer Science
ISBN
9783319148953
ISSN
0302-9743
e-ISSN
—
Number of pages
12
Pages from-to
135-146
Publisher name
Springer International Publishing
Place of publication
Neuveden
Event location
Telč, Česká republika
Event date
Jan 1, 2014
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)