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.