With the growth of multi-core processing and concurrentprogramming in modern computing systems, there is a great need todevelop effective verification techniques for concurrent programs. Staticanalysis techniques have been shown effective for finding data races, butsuffer from a general problem of too many false alarms. Dynamic tech-niques like testing have also shown promise, but provide limited coverageover the state space including all possible thread interleavings. Modelchecking alone cannot scale. However, it works better in combinationwith these techniques, with the potential of finding real error traces onone hand and better coverage on the other. In this talk, I will describe ourrecent advances in concurrent dataflow analysis, symbolic model checkingwith partial order reduction, and dynamic techniques for verifying con-current programs. These techniques have been implemented in a unifiedverification platform, currently targeted at multi-threaded C programs.I will also report on our experiences on some challenging examples fromthe public domain and the industry.
展开▼
