Interface Grammars for Modular Software Verification

Google 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