Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization

ABSTRACT. Bounded model checking (BMC) has successfully been used for many practical program verification problems, but concurrency still poses a challenge. Here we describe a new approach to BMC of sequentially consistent C programs using POSIX threads. Our approach first translates a multi-threaded C program into a non-deterministic sequential C program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. It then re-uses existing high-performance BMC tools as back-ends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of non-determininsm, so that it produces tight SAT/SMT formulae, and is thus very effective in practice: our implementation won the the concurrency category of SV-COMP14. It solved all verification tasks successfully and was 30x faster than the best tool with native concurrency handling.