Interface Grammars for Modular Software Verification
4Google Tech Talks
June, 4 2008
ABSTRACT
Verification techniques that rely on state enumeration (such as model
checking) face two important challenges: 1) State-space explosion:
exponential increase in the state space with the increasing number of
components. 2) Environment generation: modeling components that are either not available for analysis, or that are outside the scope of the verification tool at hand. We propose a semi-automated approach for attacking these two problems. In our approach, interfaces for the components that are outside the scope of the current verification effort are specified using an interface specification language based on grammars. Specifically, an interface grammar for a component specifies the sequences of method invocations that are allowed by that component. We have 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 can be 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.
Speaker: Tevfik Bultan
Associate Professor, Vice Chair
Department of Computer Science
University of California, Santa Barbara