EECS 298-11: CAD Seminar Wednesday, January 24, 1995, 5pm 531 Cory Hall, Hogan Room New Trace Theory Results Applied to Model-Checking Doron Peled AT &T Bell Laboratories Murray Hill, NJ Trace theory deals with formal languages that are closed under commuting some given pairs of letters. It was studied in the past in connection with formal language theory, the semantics of concurrent programs and Petri-nets theory. It was also recognized to be important in relation to automated program verification (model-checking) as it suggests an efficient algorithm to alleviate the most important obstacle of this field, namely, that of the state space explosion. In this talk I will survey some recent results relating trace and automata theory. Besides the independent importance of these results to trace theory, I will show how these results are put into use in automated program verification. Namely, how they allow efficient model-checking algorithms, or, in some other cases, how they can be used to show that no efficient algorithm is unlikely to exist. This talk will assume only very basic knowledge about automata theory. Next Seminar: Jan 31: Vigyan Singhal, Cadence Berkeley Labs