Aarti Gupta (NEC Labs America), Enhancing Software Model Checking with Static Program Analysis

Model checking has been used successfully in practice for verifying complex hardware designs, communication protocols, and more recently software programs. Typically, the approach for software programs is to automatically derive a verification model for the program behavior, on which back-end model checking is performed using state-of-the-art constraint solvers. However, the derived verification models are either too coarse for accurate verification or too large even for the most advanced solvers, including SAT, BDDs, and arithmetic solvers. In our framework for verifying C programs, we use highly accurate modeling of program behavior, combined with static program analysis to reduce the sizes of the derived models and to further constrain the state space search during back-end model checking. Specifically, we use program slicing, range analysis, invariant generation, predicate abstraction and model checking within a unified framework. In this talk, I will focus on the interplay between the various modeling and analysis techniques and the back-end solvers. I will also describe some practical experiences with our prototype software verification platform called F-Soft.