学院概况

讲座信息:Frontiers in Formal Methods(形式化方法前沿问题)

发布时间:2011-10-19

信息来源:

主题: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