01 · 计算人生
成果背后的人
约瑟夫·西法基斯独立开创模型检测，发展验证有限状态系统行为的方法。他在法国把形式模型与分析持续和环境交互的系统的工具联系起来，并推动建立 Verimag 实验室，后来研究嵌入式系统的严格设计。他对共同获奖成果的贡献同时涉及验证理论与可靠反应式系统的实际构造。
理解这项贡献
埃德蒙·克拉克、E. 艾伦·爱默生和约瑟夫·西法基斯发展了模型检测。有限模型描述系统状态及其转换，逻辑性质说明应当满足什么。算法探索模型，并能返回展示要求如何失败的反例。
为什么重要
自动验证成为在硬件和软件中发现隐蔽缺陷的实用工具。