Title: Bounded Model Checking with SAT/SMT

Speaker: Edmund M. Clarke

Time: 10am, Thursday Oct 17

Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, CAS.

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.