Bounded Model Checking of Lockless Programs

In this thesis we explore the potential of bounded model checking for verifying concurrent programs including the target architecture's memory ordering habits. Due to the complexity of actual processors, we devise a highly simplified virtual machine model and show that the addition of store buffers is sufficient to imitate the behaviour of current x86 implementations. After designing a formal framework for the execution of arbitrary programs on this virtual machine, encodings of the corresponding model checking problems in two different SMT formats are developed. We then present ConcuBinE, a tool for automating the encoding and evaluation of generated SMT formulas using state-of-the-art solvers and show the feasibility of our approach through a variety of experiments.