01 · 计算人生
成果背后的人
E. 艾伦·爱默生与埃德蒙·克拉克共同发展模型检测，展示如何自动检查有限状态系统的时态逻辑性质。他强调验证的逻辑基础，以及系统可能的执行过程与所需保证之间的关系。他在得克萨斯大学奥斯汀分校继续研究形式化方法，并与克拉克、约瑟夫·西法基斯共同获奖。
理解这项贡献
埃德蒙·克拉克、E. 艾伦·爱默生和约瑟夫·西法基斯发展了模型检测。有限模型描述系统状态及其转换，逻辑性质说明应当满足什么。算法探索模型，并能返回展示要求如何失败的反例。
为什么重要
自动验证成为在硬件和软件中发现隐蔽缺陷的实用工具。