Automated Analysis and Verification Research Group (VeriFIT) Brno University of Technology (BUT)
FIT spiral-of-death

DA-BMC

A Tool Chain Combining Dynamic Analysis and Bounded Model Checking

Home Tool Description Download
What is it about?

Despite the constantly growing pressure on quality of software applications, many software error still appear in the field. One class of errors which can be found in software applications more and more frequently are concurrency-related errors, which is a consequence of the growing use of multi-core processors. Such errors are hard to find by testing since they may be very unlikely to appear. One way to increase chances to detect such an error is to use various dynamic analyses, that try to extrapolate the witnessed behaviour and give a warning about possible error even if such an error is not really witnessed in any testing run. A disadvantage of such analyses is that they often produce false alarms. To void false alarms, one can use model checking based on a systematic search of the state space of the given program, but this approach is very expensive. The DA-BMC tool chain tries to combine advantages of both dynamic analysis and (bounded) model checking.

We concentrate on programs written in Java, so we use the Java PathFinder (JPF) model checker to replay traces and perform bounded model checking (BMC). To record traces of various programs, we use the infrastructure provided by the IBM Contest tool and provide a listener which records various program events used to replay the execution.

Main features
  • Recording a trace using the infrastructure provided by the IBM Contest tool.
    • It is possible to select which program events should be recorded.
  • Replaying a trace by navigating the JPF model checker through the state space of the given program according to the recorded trace.
    • DFS or BFS search strategy can be used.
    • More than one path corresponding to the recorded trace can be searched.
  • Performing bounded model checking (BMC) around suspicious states.
    • The number of states backtracked before performing BMC and the maximum depth of BMC can be set.
Authors
Acknowledgement

This work is supported by the Czech Science Foundation (projects GD102/09/H042 and P103/10/0306), the Czech Ministry of Education (projects COST OC10009 and MSM 0021630528), the European Commission (project IC0901), and the Brno University of Technology (project FIT-S-10-1).

Vendula Hrubá (ihruba AT fit.vutbr.cz), Jan Fiedor (ifiedor AT fit.vutbr.cz)