Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers

Context-bounded analysis is an attractive approach to verification of concurrent programs. Bounding the number of contexts executed per thread not only reduces the asymptotic complexity, but also the complexity increases gradually from checking a purely sequential program. Lal and Reps [14] provided a method for reducing the context-bounded verification of a concurrent boolean program to the verification of a sequential boolean program, thereby allowing sequential reasoning to be employed for verifying concurrent programs. In this work, we adapt the encoding to work for systems programs written in C with the heap and accompanying low-level operations such as pointer arithmetic and casts. Our approach is completely automatic: we use a verification condition generator and SMT solvers, instead of a boolean model checker, in order to avoid manual extraction of boolean programs and false alarms introduced by the abstraction. We demonstrate the use of field slicing for improving the scalabil...

• Type: Conference
• Year: 2009
• Where: CAV
• Authors: Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric
• Keywords: Boolean Model Checker, CAV 2009, Concurrent Boolean Program, Formal Methods, Sequential Boolean Program