VERIMAG
25 juin 2009 - 10h00
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
par Zvonimir Rakamaric de University of British Columbia
Abstract: 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 slowly from checking a purely sequential program.
Lal and Reps 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
scalability and (in some cases) coverage of our checking. We evaluate
our tool STORM on a set of real-world Windows device drivers, and
have discovered bugs that could not be detected by extensive
application of previous tools.
