学院概况

名家讲坛开讲(图灵奖得主Edmund M. Clarke): Frontiers in Formal Methods

发布时间:2011-10-17

信息来源:

讲座主题:Frontiers in Formal Methods(形式化方法前沿问题)
主办单位:2003网站太阳集团首页欢迎您
协办单位:2003网站太阳集团首页欢迎您哲学系逻辑语言与认知中心
演讲嘉宾:Professor Edmund M. Clarke
                Carnegie Mellon University, USA
讲座地点:理科一号楼1131
讲座时间:2011年10月21日(星期五)上午10:00--11:30

讲座内容简介:
"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.