主题：Frontiers in Formal Methods（形式化方法前沿问题）

报告人：Professor Edmund M. Clarke Carnegie Mellon University, USA

时间：2011年10月21日（星期五）上午10：00--11：30

地点：理科一号楼1131

讲座内容简介：

"Formal Methods" is the study of mathematical and logical techniques for the specification, development, and verification of computer systems. My research group has developed a formal method called "temporal logic model checking". In this approach specifications are expressed in a propositional temporal logic, while circuits and protocols are modeled as state-transition systems. An efficient search procedure is used to determine automatically if a specification is satisfied by a transition system. In this talk, I will focus on explaining the importance of efficient decision procedures for various logics (SAT/SMT solvers) in model checking tools, and introduce current directions in extending model checking to handle more complex models such as cyber-physical systems.

报告人简介：

Edmund M. Clarke is a computer scientist noted for developing model checking, a method for formally verifying hardware and software systems. He is the FORE Systems University Professor of Computer Science at Carnegie Mellon University, and a winner of the 2007 Association for Computing Machinery A.M. Turing Award