Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)

Dartagnan is a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnan but taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnan performs an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnan works on Boogie code. The C programs of the competition are translated internally to Boogie using SMACK.Peer reviewe