埃德蒙·克拉克（Edmund Clarke）

埃德蒙·克拉克（Edmund Clarke）是美国计算机科学家、卡内基梅隆大学教授，因与合作者开创模型检验技术、推动形式化验证走向实用而获得2007年图灵奖。

概述

克拉克1945年生于美国，长期从事程序验证研究。上世纪八十年代初，他与学生提出模型检验方法，让计算机能够自动、穷尽地检查一个系统模型是否满足给定的逻辑规范，从而在设计阶段发现潜在错误。这一技术使形式验证从纸面证明变为可自动化的工程工具。

核心特点

• 自动化：无需人工构造证明，由算法遍历系统所有可能状态。
• 基于时序逻辑：用时序逻辑描述系统应满足的性质，如安全性与活性。
• 反例生成：当性质不成立时给出具体的错误执行路径，便于调试。
• 符号化技术：借助二元决策图和可满足性求解应对状态空间爆炸问题。

应用场景

模型检验被广泛用于集成电路和处理器设计验证，帮助芯片厂商在流片前发现逻辑缺陷，避免代价高昂的召回。它也用于通信协议、嵌入式控制、航空航天和铁路信号等安全关键系统的验证，以及并发软件的死锁与竞态检测。

常见问题

问：模型检验和软件测试有何区别？答：测试只能验证有限的输入样例，无法覆盖全部情况；模型检验则在数学模型上穷尽所有状态，能给出性质成立的完整保证或明确的反例。

问：什么是状态空间爆炸？答：指系统状态数随组件增多呈指数增长，导致检验难以完成。克拉克等人发展了符号化和抽象等技术来缓解这一难题。