图灵奖得主、模型检测之父Allen Emerson去世，享年70岁
10 月 16 日，因将模型检测技术发展为一张高效的验证方法而获得 2007 年图灵奖的 Allen Emerson 永远离开了我们。
图灵奖得主、形式化研究方法的巨擘 Allen Emerson，刚刚不幸去世。 
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 透露了自己转而从事计算机科学的原因。
他对建立程序正确性的形式化方法的兴趣，可以追溯到大学时期。
并从 Tony Hoare 在 ACM 上发表的一篇题为「Proof of Program: Find」论文中受到了启发。