Detail publikace

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

Originální název

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

Anglický název

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

Jazyk

en

Originální abstrakt

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.

Anglický abstrakt

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{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",
  annote="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.",
  address="NEUVEDEN",
  chapter="91449",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="7186",
  volume="2012",
  year="2012",
  month="august",
  pages="1--5",
  publisher="NEUVEDEN",
  type="journal article - other"
}