Journal article

 
Fiedor, J., Hrubá, V., Křena, B., Vojnar, T.: DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, In: Lecture Notes in Computer Science, Vol. 2012, No. 7186, DE, p. 5, ISSN 0302-9743
Publication language:english
Original title:DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking
Title (cs):DA-BMC: Nástroj kombinující dynamickou analýzu a omezený model checking
Pages:5
Place:DE
Year:2012
URL:http://www.springerlink.com/content/l436655534440046/
Journal:Lecture Notes in Computer Science, Vol. 2012, No. 7186, DE
ISSN:0302-9743
Keywords
dynamic analysis, bounded model checking, tool support
Annotation
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.
BibTeX:
@ARTICLE{
   author = {Jan Fiedor and Vendula Hrubá and Bohuslav Křena and Tomáš
	Vojnar},
   title = {DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded
	Model Checking},
   pages = {5},
   journal = {Lecture Notes in Computer Science},
   volume = {2012},
   number = {7186},
   year = {2012},
   ISSN = {0302-9743},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9726}
}