EECS 298-11: Special CAD Seminar Monday, April 22, 1996, 5pm 531 Cory Hall, Hogan Room Note special day, Monday instead of Wednesday Deductive Model Checking Henny Sipma and Tomas Uribe Stanford University We present an extension of classical tableau-based model checking procedures to the case of infinite-state systems, using deductive methods in an incremental construction of the behavior graph. Logical formulas are used to represent infinite sets of states in an abstraction of this graph, which is repeatedly refined in the search for a counterexample computation, ruling out large portions of the graph before they are expanded to the state-level. This can lead to large savings, even in the case of finite-state systems. Only local conditions need to be checked at each step, and previously proven properties can be used to further constrain the search. Although the resulting method is not always automatic, it provides a flexible and general framework that may be used to integrate a diverse number of other verification tools. Upcoming seminars: April 24: Fong Pong, Sun Microsystems April 26 (Friday 2pm): Peter Kopke, Cornell May 1: John Marren, Alex. Brown & Sons May 8: Ganesh Gopalakrishnan, Univ. of Utah May 10 (Friday 11AM): Dhiraj Pradhan, Texas A & M Univ.