Sciweavers

CAV
2009
Springer

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

14 years 3 months ago
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...
Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamari
Added 25 Nov 2009
Updated 25 Nov 2009
Type Conference
Year 2009
Where CAV
Authors Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric
Comments (0)