Publication result detail

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

DUDKA, V.; FIEDOR, J.; KŘENA, B.; VOJNAR, T.

Original Title

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

English Title

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

Type

Peer-reviewed article not indexed in WoS or Scopus

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.

English 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

Key words in English

dynamic analysis, bounded model checking, tool support

Authors

DUDKA, V.; FIEDOR, J.; KŘENA, B.; VOJNAR, T.

RIV year

2013

Released

02.08.2012

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Volume

2012

Number

7186

State

Federal Republic of Germany

Pages from

1

Pages to

5

Pages count

5

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/"
}