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:

10am, Tuesday Oct 15: Model Checking and the Curse of Dimensionality

10am, Wednesday Oct 16: Symbolic Model Checking with Ordered Binary
Decision Diagrams

10am, 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.