Glass Box Software Model Checking.

Model checking is a formal verification technique that exhaustively tests a piece of hardware or software on all possible inputs (usually up to a given size) and on all possible nondeterministic schedules. For hardware, model checkers have successfully verified fairly complex finite state control circuits with up to a few hundred bits of state information; but not circuits in general that have large data paths or memories. Similarly, for software, model checkers have primarily verified control-oriented programs with respect to temporal properties; but not much work has been done to verify data-oriented programs with respect to complex data-dependent properties. This dissertation presents glass box software model checking, a novel software model checking approach that achieves a high degree of state space reduction in the presence of complex data-dependent properties. Our key insight is that there are classes of operations that affect a program's state in similar ways. By discovering these similarities, we dramatically reduce the state space of our model checker by checking each class of states in a single step. To achieve this state space reduction, we employ a dynamic analysis to detect similar state transitions and a static analysis to check the entire class of transitions. These analyses employ a symbolic execution technique that increases their effectiveness. We also present a modular extension to glass box software model checking, to further improve the efficiency of checking large programs composed of multiple modules. In a modular checking approach program modules are replaced with abstract implementations, which are functionally equivalent but vastly simplified versions of the modules. We also apply the glass box model checking technique to the problem of checking type soundness. Since proving type soundness can be extremely difficult, a model checking approach takes a considerable burden off the language designer. Our experimental results indicate that glass box model checking is efficient and effective at checking a variety of programs and properties, including program invariants, equivalence to an abstraction, and type soundness. Comparisons with other model checking techniques show that our technique is more efficient at checking these programs and properties.PhDComputer Science & EngineeringUniversity of Michigan, Horace H. Rackham School of Graduate Studieshttp://deepblue.lib.umich.edu/bitstream/2027.42/86472/1/roberme_1.pd