Přístupnostní navigace
E-application
Search Search Close
Publication detail
DUDKA, V. FIEDOR, J. KŘENA, B. VOJNAR, T.
Original Title
DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking
Type
journal article - other
Language
English
Original Abstract
This paper presents the DA-BMC tool chain that allows one to combine dynamic analysis and bounded model checking for finding synchronisation errors in concurrent Java programs. The idea is to use suitable dynamic analyses to identify executions of a program being analysed that are suspected to contain synchronisation errors. Some points in such executions are recorded, and then the executions are reproduced in a~model checker, using its capabilities to navigate among the recorded points. Subsequently, bounded model checking in a vicinity of the replayed execution is used to confirm whether there are some real errors in the program and/or to debug the problematic execution of the program.
Keywords
dynamic analysis, bounded model checking, tool support
Authors
DUDKA, V.; FIEDOR, J.; KŘENA, B.; VOJNAR, T.
RIV year
2012
Released
2. 8. 2012
ISBN
0302-9743
Periodical
Lecture Notes in Computer Science
Year of study
Number
7186
State
Federal Republic of Germany
Pages from
1
Pages to
5
Pages count
URL
http://www.springerlink.com/content/l436655534440046/
BibTex
@article{BUT91449, author="Vendula {Dudka} and Jan {Fiedor} and Bohuslav {Křena} and Tomáš {Vojnar}", title="DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking", journal="Lecture Notes in Computer Science", year="2012", volume="2012", number="7186", pages="1--5", issn="0302-9743", url="http://www.springerlink.com/content/l436655534440046/" }