Jin Yang Intel Strategic CAD Lab

Generalized Symbolic Trajectory Evaluation: Essence and a Case Study

Symbolic Trajectory Evaluation (STE) is a lattice-based model checking approach based on symbolic simulation. It offers an alternative to 'classical' symbolic model checking which, within its domain of applicability, is often easier to use and more efficient. However, it can only express and verify properties over finite time intervals.

GSTE is a generalization of STE that can verify all w regular properties while maintaining the benefits of STE. In the first part of this talk we will show the essence of specification and verification with GSTE. The second part presents a queue verification case study with GSTE.

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

Amit Goel is a Ph.D. student in ECE at Carnegie Mellon University. He received a B.Tech. in Electrical Engineering from the Indian Institute of Technology, Kanpur in 1998 and his M.S. degree from CMU in 2000.