EECS 298-11: Special CAD Seminar Monday, April 29, 1996, 5pm 400 Cory Hall, Hughes Room Experiences with Reduction Hierarchies Orna Kupferman AT&T Bell Laboratories, Murray Hill In the automata-theoretic approach to computer aided verification of coordinating processes, we check whether n processes P1,P2,...,Pn perform a certain task T by solving the language containment problem L(P1) \cap L(P2) \cap ... \cap L(Pn) \subseteq L(T). Conventional methods for solving this problem are doomed to fail, as the size of the product P1 * P2 * ... * Pn is very big (at least exponential in n). In 1993, Bob Kurshan suggested the method of Reduction Hierarchies as a heuristic for solving this problem. In the talk I will describe the heuristic and our efforts to understand when and how it can be used effectively. This is a joint work, in progress, with Bob Kurshan. Upcoming seminars: May 1: John Marren, Alex. Brown & Sons May 3 (11AM): Sinisa Srbljic, AT&T, U of Toronto, U of Zagreb Models for Performance Prediction of Coherence Protocols May 8: Ganesh Gopalakrishnan, Univ. of Utah May 10 (Friday 11AM): Dhiraj Pradhan, Texas A & M Univ.