01 · 计算人生
成果背后的人
埃德蒙·克拉克推动形式化验证发展为自动模型检测。他与 E. 艾伦·爱默生展示如何检查有限状态系统的时态性质，后来处理实际软硬件中巨大的状态空间。他在卡内基梅隆发展更具扩展性的验证方法和工具，把数学规格与自动寻找错误、获取正确性证据的方法联系起来。
理解这项贡献
埃德蒙·克拉克、E. 艾伦·爱默生和约瑟夫·西法基斯发展了模型检测。有限模型描述系统状态及其转换，逻辑性质说明应当满足什么。算法探索模型，并能返回展示要求如何失败的反例。
为什么重要
自动验证成为在硬件和软件中发现隐蔽缺陷的实用工具。