Kedar Namjoshi (Bell Labs), Incremental Model Checking

In programming practice, a program is modified continuously, either to fix errors or to add new features. Current model checking tools pay little or no attention to this process, analyzing each input program independently of the others. The objective of "incremental" model checking is to match the programming process by analyzing program increments vs. complete programs. The key to this method is a data structure that stores a "proof" of a model checking result. I will describe such an algorithm for checking safety of recursive programs, and discuss an application to static analysis. By speeding up analysis time, often by an order of magnitude, incremental methods can form a practical basis for "correct-by-construction" programming.