时间：21日（星期五）上午10：00--11：30
地点：理科一号楼1131
演讲人： Professor Edmund M. Clarke
       （Carnegie Mellon University, USA)

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

摘要："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. The technique has been used in the past to find subtle errors in various systems, and widely applied in the hardware and software industry. 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.