2007年图灵奖颁发给了两位计算机界的重要人物：Edmund M. Clarke和E. Allen Emerson。这是对于形式化验证领域的巨大肯定。他们的研究成果让计算机科学家们能够利用自动化工具检查硬件和软件的正确性。这项技术的发展，不仅大大增强了计算机系统的可靠性，而且为真正的机器智能和自主地软件和机器人的开发铺平了道路。

Edmund M. Clarke和E. Allen Emerson的主要成就是发明了一种名为模型检查的算法，这个算法革新了计算机科学的一个经典问题：如何检查一个系统是否正确地执行。在大型系统中，特别是安全和航空航天领域，这个问题至关重要，因为错误可能引起人员伤亡和损失。

模型检查是一种通过规范化描述系统，然后在模型上进行状态空间搜索，来进行错误检查的技术。在模型检查中，一个系统被转化为一个有限状态机模型，然后通过形式化的数学方法进行检查。如果通过模型检查找到了错误，那么就可以对代码进行修改，以确保程序能够正确地执行。

这项技术可以应用于各种不同的软件和系统。例如，它可以用于检查安全性和信任性软件，也可以用于测试汽车和到航空飞机的控制系统的准确性。

这个算法的成功是基于两个关键创新。首先，他们引入了一个名为公平性的概念，在检查状态转换树的同时，确保每个状态都被访问。其次，他们使用了一种被称为二叉决策图的数据结构来存储和表示状态。这个简单的结构在搜索状态空间时可以避免计算机无法处理的状态的产生。

两位得奖人的成就，证实了形式方法对于构建更加可靠软件的重要性。他们的成就也获得了工业界的广泛认可，已经被许多公司和机构应用于产品开发中。

总的来说，这个奖项的意义超出了这两位获奖者的个人和研究团队的篇幅。它代表了计算机科学领域的前沿技术，标志着大型系统中的可靠性和正确性的重要进步。