Beyond Testing: Static Analysis by Bounded Model Checking.

Increasingly often, the high degree of sophistication of modern software systems limits the effectiveness of testing as a reliability assessment methodology. Rigorous verification procedures to be seamlessly integrated in the software development life cycle are therefore very sought after. This talk introduces program verification, and in particular static analysis, from a practical standpoint while looking at the specific case of finding bugs in imperative programs. On several classes of instances such a task can be automated, to a reasonably large extent and with acceptable performance, by using state-of-the-art bounded model checking. For example, this strategy has been shown to be effective to spot subtle bugs in device drivers and embedded software. We sketch the general schema and describe the anatomy of a typical SAT-based bounded model checker. We discuss some of the ongoing theoretical challenges that would need to be addressed in order to extend the approach to other classes of programs and kinds of analyses. We identify a few major technical hurdles on the way to industrial strength.