Verification of multi-threaded C programs

Verifying the correctness of a program involves providing a guarantee, in the form of a logical proof, that the program is free of bugs for all possible inputs. It is therefore able to provide software developers and users with a much higher degree of confidence in a program's ability to perform its job than traditional testing, due to the fact that it produces certainty rather than empirical evidence of a program's partial correctness, something which is especially important when that program is responsible for large sums of money or human lives. Multi-threaded programs are able to take advantage of modern multi-core architectures more effectively than single-threaded programs but introduce challenges both to the author and the verifier. Concurrent programs are regarded as being more difficult to write and understand than traditional sequential programs by developers due to the large number of ways in which the multiple threads may interact throughout a program's execution. As such, the ability to formally verify this type of software is perhaps even more valuable than traditional single-threaded programs. For verification, the combinatorial number of ways in which the operations of each thread may be interleaved by a non-deterministic scheduler introduces the problem of state-space explosion. Here, we describe a method for adapting trace abstraction refinement, an existing technique for verification of single-threaded programs for application to multi-threaded programs in combination with an approach to reduce the state space of the program based on dynamic partial order reduction. We apply this method to enable the verification of C programs, building on the work on this topic by Cassez and Zeigler.