NOTE: This announcement constitutes two changes: 1) The speaker for this week's CAD seminar has changed. The original speaker, Raul Camposano, will be rescheduled for later in the semester. 2) Henzinger's talk was orinally scheduled for room 277 Cory. EECS 298-11: CAD Seminar Wednesday, March 22, 5pm 531 Cory Hall, Hogan Room Computer-Aided Verification of Infinite-State Systems Thomas A. Henzinger Cornell Univ. Over the past decade, Computer-Aided Verification has matured into a useful collection of algorithms for the analysis of concurrent systems with finite state spaces, such as boolean circuits and communication protocols. Verification goes one step beyond simulation by performing a systematic, rather than sampling, analysis of a given state space. One of the main lessons in verification teaches us to represent large state sets implicitly, by symbolic constraints, rather than explicitly, by enumerating states. We show that symbolic verification techniques apply not only to large finite state spaces but also to infinite state spaces, including euclidean state spaces with continuous dynamics. Our work brings real-time protocols (with real-valued clocks) and process-control systems (with real-valued environment parameters) within the scope of verification tools. We use hybrid automata as a paradigm for infinite-state systems. A hybrid automaton is a mathematical model for a digital system that interacts with an analog environment. On the practical side, we identify linear hybrid automata as a class of infinite-state systems that can be analyzed automatically. Our symbolic model checker HyTech computes sufficient and necessary conditions under which a collection of linear hybrid automata satisfies a temporal-logic requirement. We illustrate the application of HyTech by analyzing the Philips audio control protocol, a real-time protocol with drifting clocks. On the theoretical side, we prove both positive and negative results about the verifiability of hybrid automata by extending the theory of discrete transition systems to continuous dynamical systems. For example, by defining bisimulation relations on hybrid state spaces, we obtain the class of hybrid automata with finite bisimulations as an interesting generalization of timed automata. March 29 - NO SEMINAR, due to Spring break April 3 - Raul Camposano (NOTE special day) "Higher Level Design Tools" April 5 - Dave Patterson, UC Berkeley "A Case for NOW" April 12 - Ed Clarke, CMU April 19 - Jacob White, MIT "How Matrix-Free Iterative Methods Have Changed Computer Simulation of Circuits, Interconnect, Packaging, and Micro-Electro-Mechanical Systems"