Interface grammars for modular software verification

Applying model checking techniques directly to programs has shown extensive promise; however, two related problems hinder applicability of model checking to software on a wider scale. First, the state space explosion problem (i.e., an exponential increase in the search space by increasing number of variables and concurrent components) limits the scalability of model checking techniques and second, the environment generation problem (i.e., finding models for parts of software that are outside the scope of the model checker) limits the applicability of model checking to the domains where such environment models are available. I propose a semi-automated approach to attack the above mentioned problems. Specifically, I propose an interface specification language and require the users to write interface specifications for components of a program that are outside the scope of the current verification effort. My interface specification language allows a user to write an interface grammar for a component to specify the constraints on the ordering of calls made by the program to that component. This approach enables modeling of nested call structures that cannot be expressed by interfaces based on finite state machines. I built an interface compiler that takes the interface grammar for a component as input and generates a stub for that component. The stub generated from the interface grammar of a component is used to replace that component during state space exploration, either to assuage the state space explosion, or to provide an executable environment for the component that is being verified.