图灵奖：约瑟夫·斯发基斯（2007）

图灵奖是计算机界最负盛名的奖项，有“计算机界诺贝尔奖”之称。”图灵奖”系列将介绍历届获奖者。每周二更新，本文为第 53 期。图灵奖：约瑟夫·斯发基斯（2007）

文章来自微信公众号“科文路”，欢迎关注、互动。转发须注明出处。

本文来自 Wiki: Joseph Sifakis，翻译基于 谷歌翻译.

模型检查 Model-Checking

约瑟夫·斯发基斯（英语：Joseph Sifakis，希腊语：Ιωσήφ Σηφάκης，1946年12月26日—），希腊计算机科学家。他曾担任清华大学（2011-2012 年）和南方科技大学（2019 年）的客座教授。

他于 2007 年获得图灵奖。

其图灵奖颁奖词为“表彰其与Edmund Clarke和E. Allen Emerson一起，在将模型检查（Model-Checking）发展为一种高度有效的验证技术方面的作用，该技术被广泛应用于硬件和软件行业”。（Together with Edmund Clarke and E. Allen Emerson, for their role in developing Model-Checking into a highly effective verification technology that is widely adopted in the hardware and software industries. ）

生平

斯发基斯 1946 年出生于克里特岛伊拉克利翁，现居法国。他曾就读于雅典国立技术大学（National Technical University of Athens）电气工程专业，以及格勒诺布尔大学（University of Grenoble）的计算机科学专业。

1974 年，他在格勒诺布尔大学获得工程学博士学位，并于 1979 年在该大学获得国家博士（state doctorate）学位。

他是格勒诺布尔附近 VERIMAG 实验室国家科学研究中心的创始人，现为该中心的名誉研究主任。

斯发基斯担任 VERIMAG 主任十四年。VERIMAG 最初是 CNRS 和 Verilog SA 之间的混合工业实验室，与空中客车和施耐德电气合作开发了安全关键系统开发的方法和工具，特别是基于 Lustre 语言的 SCADE 同步编程环境。Sifakis 与 Thomas Henzinger 合作验证了定时和混合系统，并与 Amir Pnueli 和 Oded Maler 合作合成了定时系统。他参与了 IF 工具集、Kronos、CADP 和 TGV 等验证工具的开发，并开发了使用抽象技术应对状态爆炸的理论。

斯发基斯致力于系统验证和形式化方法在系统设计中的应用。在他攻读博士学位期间，他研究了后来被称为模型检查的算法验证方法的原理。1982 年，Jean-Pierre Queille 在博士论文中应用了这项技术来开发 CESAR 验证工具。

~~

都看到这儿了，不如关注每日推送的“科文路”、互动起来~

至少点个赞再走吧~

觉得还不错？可以在公众号菜单栏找到“赞赏”入口~