Ernest Allen Emerson II，1954年6月2日-2024年10月16日2007年，他与Edmund Clarke和Joseph Sifakis一起，因将模型检测技术（Model Checking）发展为一种高效的验证技术，并被硬件和软件行业广泛采用，而获得图灵奖。除了图灵奖，Emerson还与Randal Bryant、Clarke和Kenneth L. McMillan一起获得了1998年的ACM Paris Kanellakis奖，以表彰他们在开发符号模型检测方面的贡献。授奖理由如下：「他们发明了符号模型检测，这是一种正式检查系统设计的方法，在计算机硬件行业得到广泛使用，并且在软件验证和其他领域也开始显示出重要的应用前景。」他对时序逻辑和模态逻辑的贡献，包括引入计算树逻辑（CTL）及其扩展CTL*，这些技术被用于并发系统的验证。此外，他还与其他研究者一起开发了符号模型检测，用于解决许多模型检测算法中出现的组合爆炸问题，因此获得了广泛认可。
生平
Allen Emerson出生于美国得克萨斯州达拉斯，从小便对科学、数学话题非常感兴趣。在上公立学校之前的几年里，他自学了微积分。在高中时期，Emerson学习了一门计算机编程课，并学习了GE Mark I分时系统的基础知识。随后，他又自学了BASIC、Fortran和ALGO 60编程语言，并在Burroughs B5500大型计算机上运行了程序。1976年，Emerson在得克萨斯大学奥斯汀分校获得了数学学士学位。他继续在哈佛大学研究生院学习，并于1981年获得了应用数学（计算机科学）博士学位。此后不久，他便以教员的身份，加入了得克萨斯大学奥斯汀分校，并一直在此任教。此后担任荣休教授和荣休校董事主席。
4年前的采访中，Emerson透露了自己转而从事计算机科学的原因。
，时长03:01
他对建立程序正确性的形式化方法的兴趣，可以追溯到大学时期。
并从Tony Hoare在ACM上发表的一篇题为「Proof of Program: Find」论文中受到了启发。
论文地址：https://dl.acm.org/doi/pdf/10.1145/362452.362489另外，还有一个启发性因素是Zohar Manna在德克萨斯大学发表的演讲——不动点和Tarski-Knaster定理。Emerson还对J. W. De Bakker、W. P De Roever和Edsger W. Dijkstra关于谓词Transformer的工作感兴趣。
模型检测
20世纪80年代初，Emerson与他的博士导师Edmund M. Clarke共同开发了验证有限状态系统对形式规范的技术。他们创立了一种自动化质量保证方法的技术概念，该方法检查一个名义上有限状态并发系统是否提供其规范的模型（即满足其规范）。他们为这个概念创造了「模型检测」这个术语，在欧洲，Joseph Sifakis 独立发现了类似的想法。这里「模型」一词的含义与数理逻辑中模型理论的用法相符：系统被称为规范的模型。
