Three Lectures on Model Checking

Professor Edmund M. Clarke from Carnegie Mellon University has been awarded the Einstein Professorship of the Chinese Academy of Sciences in 2013, and will be visiting the State Key Laboratory of Computer Science, Institute of Software, CAS, in the week of 14-18 Oct. During the visit, Prof. Clarke will present the following three lectures:

10:00, Tuesday Oct 15: Model Checking and the Curse of Dimensionality
10:00, Wednesday Oct 16: Symbolic Model Checking with Ordered Binary Decision Diagrams
10:00, Thursday Oct 17: Bounded Model Checking with SAT/SMT

The venue for these lectures is: Lecture Room, 3rd Floor, Building #5,State Key Laboratory of Computer Science, Institute of Software, CAS.

All are welcome.

Biography:
Professor Edmund M. Clarke received a B.A. degree in mathematics from the University of Virginia in 1967, an M.A. degree in mathematics from Duke University in 1968, and a Ph.D. degree in Computer Science from Cornell University in 1976. After receiving his Ph.D., he taught in the Department of Computer Science at Duke University for two years. In 1978 he moved to Harvard University where he was an Assistant Professor of Computer Science in the Division of Applied Sciences. He left Harvard in 1982 to join the faculty in the Computer Science Department at Carnegie Mellon University, Pittsburgh, PA. He was appointed Full Professor in 1989.

In 1981 Professor Clarke and his Ph.D. student E. Allen Emerson first proposed the temporal logic CTL, used to describe properties of concurrent systems, and an algorithm to check whether a finite state concurrent system satisfies a CTL formula. This work initiated a research area termed “Model Checking”.  For the past thirty years Professor Clarke and his research group have been a driving force to push forward the research and applications of the theories and techniques of model checking. It has become one of the most important techniques for the analysis and verification of concurrent systems, and has been widely used in industrial practice.

Professor Clarke received the 2007 ACM Turing Award, along with E. Allen Emerson and Joseph Sifakis, for his role in developing Model-Checking into a highly effective verification technology, widely adopted in the hardware and software industries.

Professor Clarke was elected to the National Academy of Engineering in 2005 and to the American Academy of Arts and Sciences in 2011. He is a fellow of the ACM and the IEEE.