Result Details

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

DUDKA, V.; FIEDOR, J.; KŘENA, B.; VOJNAR, T. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7186, p. 1-5. ISSN: 0302-9743.
Type
journal article
Language
English
Authors
Dudka Vendula, Ing., DITS (FIT)
Fiedor Jan, Ing., Ph.D., DITS (FIT)
Křena Bohuslav, Ing., Ph.D., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
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

URL
Published
2012
Pages
1–5
Journal
Lecture Notes in Computer Science, vol. 2012, no. 7186, ISSN 0302-9743
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/"
}
Projects
Advanced secured, reliable and adaptive IT, BUT, Vnitřní projekty VUT, FIT-S-11-1, start: 2011-01-01, end: 2013-12-31, completed
Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit, MŠMT, COST, OC10009, start: 2010-01-01, end: 2012-12-31, running
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, start: 2010-01-01, end: 2013-12-31, running
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top