Publication Details

DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking

DUDKA Vendula, FIEDOR Jan, KŘENA Bohuslav and VOJNAR Tomáš. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. FIT-TR-2011-06, Brno: Faculty of Information Technology BUT, 2011.
Czech title
DA-BMC: Nástroj propojující dynamickou analýzu a bounded model checking
Type
technical report
Language
english
Authors
Dudka Vendula, Ing. (DITS FIT BUT)
Fiedor Jan, Ing., Ph.D. (DITS FIT BUT)
Křena Bohuslav, Ing., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

dynamic analysis, bounded model checking, verification, record and replay

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.

Published
2011
Pages
9
Publisher
Faculty of Information Technology BUT
Place
FIT-TR-2011-06, Brno, CZ
BibTeX 
@TECHREPORT{FITPUB9780,
   author = "Vendula Dudka and Jan Fiedor and Bohuslav K\v{r}ena and Tom\'{a}\v{s} Vojnar",
   title = "DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking",
   pages = 9,
   year = 2011,
   location = "FIT-TR-2011-06, Brno, CZ",
   publisher = "Faculty of Information Technology BUT",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9780"
}
Back to top