Prof. Edmund M. Clarke Visits Institute of Software

Date:2013-04-23

Prof. Clarke is a computer scientist being famous for pioneering Model Checking, a method for formally verifying hardware and software systems, in 1980s and continuously making significant contributions to the field. He is the FORE Systems University Professor of Computer Science at Carnegie Mellon University, and a co-recipient of the 2007 ACM Turing Award for his role in developing Model Checking into a highly effective verification technology.

Prof. Clarke gave a lecture at ISCAS on April 19th, 2013. The lecture was titled as “Turing’s Computable Real Numbers and Why They Are Still Important Today”. For a long time, formal verification paid little attention to computational applications that involve the manipulation of continuous quantities, even though such applications are ubiquitous. In recent years, however, there has been great interest in safety-critical hybrid systems involving both discrete and continuous behaviors, including autonomous automotive and aerospace applications, medical devices of various sorts, control programs for electric power plants, and so on. As a result, the formal analysis of numerical computation can no longer be ignored. In the talk, Prof. Clarke was focused on one of the most successful verification techniques, temporal logic model checking. He believed that the key to handling more complex systems is to make better use of the theory of the computable reals, and computable analysis more generally.

He reported their new formal method for verification of hybrid systems, combining existing discrete methods in model checking with new algorithms based on computable analysis. In particular, he also demonstrated a model checker, named dReal, which is currently underdeveloped along these lines. 

As a science educator, Prof. Clarke also showed a great passion for the education of young scientists. He encouraged young researchers to explore novel methods and combine different fields of knowledge in their research. The audience had a heated discussion with Prof. Edmund M. Clarke in the end of the lecture.

 Prof.Edmund M.Clarke reported