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 can achieve a high degree of state space reduction in the
presence of complex data. Our key insight is that there are classes of operations that
affect a program's state in similar ways. By discovering these similarities, we can
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.