Edmund Clarke is a Professor of Computer Science at Carnegie Mellon University, Turing Award winner in 2007, and "Einstein Chair Professor" of Chinese Academy of Science. He paid a visit to Suzhou Institute for Advanced Study of USTC from October 20 to 27.
Prof. Clarke is one of the founders of Model Checking, a technology in the field of formal verification. He is ACM and IEEE fellow, and also a fellow of the National Academy of Science and Engineering. Professor Clarke shared the "Turing Award" in 2007, with another two scientists, E.Allen Emerson and Joseph Sifakis, in recognition of their contributions to the foundation of the theory and technology of model checking, which, has become an effective verification method in hardware and software industry.
On October 21st morning, Prof. Clarke gave a report titled “Model Checking and the Curse of Dimensionality”. In his speech, Professor Clarke reviewed the development of model checking theory, analyzed the four typical problems encountered during the past 20 years, and explained how to solve these problems to make great breakthrough.
On the morning of October 22nd, Professor Clarke gave another lecture titled “Symbolic Model Checking with BDDs” for the staff and students at USTC-Yale High Reliable Software Joint Developing Center. Professor Clarke introduced the origin of symbolic model checking and the basic principle of the algorithm. By using the model checking algorithm, he and his students detected a flawed cache coherence protocol in the IEEE FutureBus+ Standard in 1992. October 23rd morning, Professor Clarke focused on the bounded model checking method based on the tool of SAT in his second special lecture titled "Bounded Model Checking with SAT/SMT ".
During the next few days, Professor Clarke carried out face-to-face in-depth exchanges with teachers and students of the Institute, and listened to the work of the USTC - Yale High Reliable Software Joint Developing Center and the Laboratory of Embedded Systems. Professor Clarke expressed a great interest in the research of the teams of the Suzhou Institute, and put forward valuable suggestions.
(WANG Lin, School of Computer Science and Technology)
