约瑟夫·希发基思(Joseph Sifakis)
男,希腊和法国双国籍,计算机科学家。1946年12月出生于希腊,1969年获雅典技术大学电子工程学士学位,1974年获法国格勒诺布尔大学计算机科学博士学位。2007年获国际计算机界最高奖“图灵奖”。2008年当选法国工程院院士和欧洲科学院院士,2010年当选法国科学院院士,2015年当选美国人文和科学院院士,2017年当选美国工程院外籍院士。现任法国国家科学中心主任研究员。
希发基思教授的主要研究领域是模型检测及嵌入式系统设计与验证。他在1979年提出了通过对时序逻辑公式的计值来验证并发系统性质的思想,得到了一系列理论结果,包括对含有“可能”和“必然”模态算子的分支时序逻辑的不动点刻划。在此基础上他进一步提出了带有“until”算子的分支时序逻辑来表达“公平性”。他的这些工作与卡耐基梅隆大学Clarke教授、得克萨斯大学奥斯汀分校Emerson教授同时期的工作一起,为模型检测这个研究领域的创立和发展奠定了理论基础。模型检测已被应用于计算机硬件、软件、通信协议、安全认证协议等领域,取得了巨大的成功,成为分析、验证并发系统性质的最重要的技术,被Intel、IBM、微软等公司用于日常生产实践中。由于对模型检测的开创性贡献,他与Clarke教授、Emerson教授分享了2007年图灵奖。
希发基思教授是欧洲嵌入式系统研究的先驱。嵌入式系统广泛存在于航天、航空、汽车、火车、通信、医疗、武器等安全攸关的领域。他提出了首个面向带时间分支时序逻辑TCTL的符号模型检测算法,以该算法为基础实现了适用于实时系统模型检测的验证工具Kronos。从2004年至2012年,希发基思教授担任欧盟“卓越网络” ARTIST嵌入式系统研究联盟的科学协调人,负责协调欧洲35个实时与混成系统领域研究小组的工作。
希发基思教授对中国怀有深厚的感情。他亲自指导了六名中国留学生和博士后。这些学生已成为中国科学院软件所、浙江大学、军事科学院等单位的科研骨干。在他担任欧盟ARTIST嵌入式系统研究联盟科学协调人期间,极力推动欧盟与中国在该领域的合作。在他领导下,该研究联盟从2006年至2011年在中国举办了六届嵌入式系统设计讲习班,使用欧盟的经费,邀请国际上嵌入式系统的知名专家为国内的研究生和青年学者讲课。希发基思教授频繁来中国开展学术访问,在中国科学院软件所、计算所、清华大学、北京大学、西北工业大学、东北大学、哈尔滨工业大学、华东师范大学、深圳大学、华为公司等处做学术报告。2017年8月至今, 他担任清华大学计算机学科顾问委员会委员。2019年1月开始,他出任南方科技大学杰出教授。