Abstract: Compositional verification has been long sought as a promising way of extending the applicability of symbolic model checking to larger and more relevant systems. Traditionally, this is based on the assume-guarantee paradigm. We propose a new compositional approach based on GSTE (Generalized Symbolic Trajectory Evaluation). There are two main contributions in our approach. First, we propose a specification language that allows properties to be described succinctly in a compositional algebraic manner. Second, we show a precise model checking solution for a compositional specification through automata construction, but much more importantly and practically, we develop an efficient model checking algorithm for directly verifying the compositional specification. At the end, we show the result of the our approach in the verification of a real-life micro-instruction scheduler from a state-of-the-art micro-processor.

Biography: Jin Yang is currently a senior staff researcher in Intel Strategic CAD Labs, in the area of formal verification research. His main interest is in developing and applying practical formal specification and verification technologies. He received his Ph.D. degree in Computer Science from the University of Texas at Austin in 1997 where his research interest was on the formal specification and verification of hard real time systems.