2007 埃德蒙-克拉克

shiyi18

Edmund Clarke

PHOTOGRAPHS
BIRTH:
July 27, 1945.

DEATH:
December 22, 2020.

EDUCATION:
BA, Mathematics, (University of Virginia, 1967); MA Mathematics (Duke University, 1968);Ph.D., Computer Science (Cornell University, 1976)

EXPERIENCE:
Duke University (1976–1978); Harvard University (1978–1982); Carnegie Mellon University (1982–present, including FORE Systems Professor 1995–present, University Professor 2008–present).

HONORS AND AWARDS:
Technical Excellence Award, Semiconductor Research Corporation (1995); ACM Paris Kanellakis Theory and Practice Award (1998, with Randal  Bryant, E. Allen Emerson, and Kenneth L. McMillan); IEEE Harry H. Goode Memorial Award (2004); Elected to National Academy of Engineering (2005); ACM Turing award (2007, with Emerson and Sifakis); International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning (2008); Logic in Computing Science (LICS) 2010 Test-of-Time Award for his 1990 paper, "Symbolic model checking…; Elected to the American Academy of Arts and Sciences (2011); Fellow of the ACM and IEEE; Honorary Doctorate, (Vienna University of Technology, 2012); Bower Award and Prize for Achievement in Science from the Franklin Institute (2014).



EDMUND MELSON CLARKE DL Author Profile link
United States – 2007
CITATION
Together with E. Allen Emerson and Joseph Sifakis, for their role in developing Model-Checking into a highly effective verification technology that is widely adopted in the hardware and software industries.

SHORT ANNOTATED
BIBLIOGRAPHY
ACM TURING AWARD
LECTURE VIDEO
RESEARCH
SUBJECTS
Birth and education
Edmund Melson Clarke was born on July 27, 1945. He initially studied mathematics, receiving a BA from the University of Virginia in 1967 and an MA from Duke University in 1968. But by the time he enrolled in a doctoral program at Cornell University, he had switched to computing science. At Cornell he studied under Robert Constable, a pioneer in making deep connections between mathematical logic and computing. After graduation Clarke returned to teach at Duke for two years, moving to Harvard University in 1978. He joined Carnegie Mellon University in 1982, where he is currently the FORE Systems University Professor of Computer Science and Professor of Electrical and Computer Engineering.

Clarke’s career has focused on mathematical reasoning about computer systems, with an emphasis on reasoning about the reliability of those systems. Such reasoning is necessary but very hard. A computer system executes simple operations, but those operations can occur in a staggering number of different orders. This makes it impossible for the designer to envision every possible sequence and predict its consequences. Yet every one of those sequences, no matter how infrequently executed, must be correct. If a program executes an incorrect sequence, at the very least it will waste a user’s time, while at the worst it could cause injury or loss of life.

The sequences become even more difficult to envision in systems with multiple programs running at the same time—a feature that has long been present in computer hardware and has become widespread in software since the beginning of the 21st century. Mathematical reasoning, and specifically its expression in formal logic, in principle is sufficient to describe every possible sequence and ensure that all of them are correct, even for simultaneously-running programs. In practice, however, classical mathematical reasoning is awkwardly-matched to describing the many possible execution orderings in a computer system.

Inventing model checking
Early researchers addressed this mismatch by developing logical forms better-suited to describing computer systems. One of the first was by Tony Hoare. Hoare’s logic could be used to prove that every possible execution of a system would only execute an acceptable sequence of operations. This opened the possibility that systems could be proven to perform according to specification every time, no matter the circumstances. Clarke’s early research strengthened the foundations of Hoare’s logic and extended his method. Although Hoare’s method worked for smaller systems, it was close to impossible to apply to systems of any real size. The dream of powerful, effective methods for reasoning about all possible orderings of a system remained unfulfilled.

In 1977, Amir Pnueli introduced temporal logic, an alternative logic for verifying computer systems. As the name implies, temporal logic allows explicit reasoning about time. In temporal logic it is possible to express statements such as, “This condition will remain true until a second condition becomes true”.

Clarke and his student E. Allen Emerson saw an important possibility in temporal logic: it could be directly checked by machine. Whereas Hoare’s logic required the designer to consider every detail of both the system and the argument about the system’s correctness—substantially increasing the designer’s workload—Pnueli’s logic could be implemented in a computer program. The responsibilities could be divided: the designer focused on specifying the system, while the software ensured that the proposed system would always perform correctly.

Clarke and Emerson realized that a program could exhaustively construct every possible sequence of actions a system might perform, and for every action it could evaluate a property expressed in temporal logic. If the program found the property to be true for every possible action in every possible sequence, this proved the property for the system. In the language of mathematical logic, Clarke and Emerson’s program checked that the possible execution sequences form a “model” of the specified property. Working independently, Jean-Pierre Queille and Joseph Sifakis developed similar ideas. The technology of model checking was born.

A great strength of the model checking approach is that when it detects a problem in a system design, the checker prints out an example sequence of actions that gives rise to the problem. Initial designs always get some details wrong. The error traces provided by model checking are invaluable for designers, because the traces precisely locate the source of the problems.

Averting the state space explosion
Although the 1981 paper [2] demonstrated that the model checking was possible in principle, its application to practical systems was severely limited. The most pressing limitation was the number of states to search. Early model checkers required explicitly computing every possible configuration of values the program might assume. For example, if a program counts the millimeters of rain at a weather station each day of the week, it will need 7 storage locations. Each location will have to be big enough to hold the largest rain level expected in a single day. If the highest rain level in a day is 1 meter, this simple program will have 1021 possible states, slightly less than the number of stars in the observable universe. Early model checkers would have to verify that the required property was true for every one of those states.

Systems of practical size manipulate much more data than the simple example above. The number of possible states grows as well, at an explosive speed. This rapid growth is called the state space explosion. Although early model checkers demonstrated that the technology was feasible for small systems, it was not ready for wider use.

Clarke and his student Ken McMillan had a fundamental insight: The state space explodes because the number of states a memory location can assume is much, much bigger than the size of the location itself. The memory location is compact because it encodes many potential states but only contains one at a time. Clarke and McMillan observed that this process could be applied in reverse: with the right encoding, many potential states could be represented by a single value. From the literature, McMillan found an encoding that met the twin goals of tersely encoding multiple states while at the same time permitting efficient computation of formulas in temporal logic.

The new representation dramatically reduced the storage required to represent state spaces, in turn reducing the time required to run a model checker on systems of practical size. They called these new systems symbolic model checkers. In 1995, Clarke, McMillan, and colleagues used this approach to demonstrate flaws in the design of an IEEE standard for interconnecting computer components. Before this, the reliability of such standards had only been informally analyzed, leaving many rare cases unconsidered and potential errors undiscovered. This was the first time every possible case of an IEEE standard had been exhaustively checked.

With enhancements such as these, model checking has become a mature technology. It is widely used to verify designs for integrated circuits, computer networks, and software, by companies such as Intel and Microsoft. Model checkers have been used to analyze systems whose state space (10120) is substantially larger than the number of atoms in the observable universe (around 1080). It is becoming particularly important in the verification of software designed for recent generations of integrated circuits, which feature multiple processors running simultaneously. Model checking has substantially improved the reliability and safety of the systems upon which modern life depends.

Author: Ted Kirkpatrick



埃德蒙-克拉克

照片
诞生。
1945年7月27日。

逝世。
2020年12月22日。

教育背景。
数学学士（弗吉尼亚大学，1967）；数学硕士（杜克大学，1968）；计算机科学博士（康奈尔大学，1976）。

工作经验。
杜克大学（1976-1978）；哈佛大学（1978-1982）；卡内基梅隆大学（1982年至今，包括1995年至今的FORE系统教授，2008年至今的大学教授）。

荣誉和奖项。
技术卓越奖，半导体研究公司（1995年）；ACM巴黎卡内拉基斯理论与实践奖（1998年，与Randal Bryant, E. Allen Emerson, and Kenneth L. McMillan）；IEEE哈里-H. 古德纪念奖（2004年）；当选为国家工程院院士（2005年）；ACM图灵奖（2007年，与Emerson和Sifakis共同获得）；国际自动演绎会议（CADE）Herbrand自动推理杰出贡献奖（2008年）；计算科学逻辑（LICS）2010年时间测试奖，以表彰其1990年的论文 "符号模型检查"。 当选为美国艺术与科学学院院士（2011年）；ACM和IEEE会员；荣誉博士，（维也纳科技大学，2012年）；富兰克林研究所颁发的鲍尔奖和科学成就奖（2014年）。



EDMUND MELSON CLARKE DL作者简介链接
美国 - 2007年
参考文献
与E.Allen Emerson和Joseph Sifakis一起，因其在将模型检查发展为一种高效的验证技术方面的作用而被硬件和软件行业广泛采用。

简短注释
书目
亚马逊图灵奖
讲座视频
研究
题目
出生和教育
埃德蒙-梅尔森-克拉克出生于1945年7月27日。他最初学习数学，1967年在弗吉尼亚大学获得学士学位，1968年在杜克大学获得硕士学位。但当他进入康奈尔大学的博士课程时，他已转而学习计算科学。在康奈尔大学，他师从罗伯特-康斯特布尔，他是在数理逻辑和计算之间建立深刻联系的先驱者。毕业后，克拉克回到杜克大学任教两年，于1978年转到哈佛大学。他于1982年加入卡内基梅隆大学，目前是FORE系统大学的计算机科学教授和电子与计算机工程教授。

克拉克的职业生涯专注于计算机系统的数学推理，重点是对这些系统的可靠性进行推理。这种推理是必要的，但却非常困难。一个计算机系统执行简单的操作，但这些操作可能以惊人的不同顺序发生。这使得设计者不可能设想到每一个可能的序列并预测其后果。然而，这些序列中的每一个，无论多么不经常执行，都必须是正确的。如果一个程序执行了一个不正确的序列，至少会浪费用户的时间，而在最坏的情况下，它可能会造成伤害或生命损失。

在有多个程序同时运行的系统中，序列变得更加难以设想，这一特点长期以来一直存在于计算机硬件中，自21世纪初以来在软件中变得非常普遍。数学推理，特别是其在形式逻辑中的表达，原则上足以描述每一个可能的序列，并确保所有的序列都是正确的，即使是对于同时运行的程序。然而，在实践中，经典的数学推理与描述计算机系统中许多可能的执行顺序是很难匹配的。

发明模型检查
早期的研究人员通过开发更适合于描述计算机系统的逻辑形式来解决这种不匹配。最早的一个是由Tony Hoare提出的。Hoare的逻辑可以用来证明一个系统的每一个可能的执行都只执行一个可接受的操作序列。这开辟了一种可能性，即无论在什么情况下，系统都可以被证明是按照规格执行的。克拉克的早期研究加强了霍尔逻辑的基础并扩展了他的方法。尽管Hoare的方法对较小的系统有效，但它几乎不可能应用于任何实际规模的系统。对一个系统所有可能的排序进行推理的强大而有效的方法的梦想仍未实现。

1977年，Amir Pnueli提出了时间逻辑，一种用于验证计算机系统的替代逻辑。顾名思义，时间逻辑允许对时间进行明确推理。在时间逻辑中，有可能表达这样的语句："这个条件将保持真实，直到第二个条件变成真实"。

克拉克和他的学生艾伦-爱默生在时间逻辑中看到了一个重要的可能性：它可以直接被机器检查。而Hoare的逻辑要求设计者考虑系统的每一个细节和关于系统正确性的论证--大大增加了设计者的工作量--Nnueli的逻辑可以在计算机程序中实现。责任可以划分：设计者专注于指定系统，而软件则确保所建议的系统总是能够正确执行。

克拉克和爱默生意识到，一个程序可以详尽地构建一个系统可能执行的每一个行动序列，对于每一个行动，它可以评估一个用时间逻辑表达的属性。如果程序发现该属性对每个可能的序列中的每个可能的行动都是真的，这就证明了该系统的属性。在数理逻辑的语言中，Clarke和Emerson的程序检查了可能的执行序列是否形成了指定属性的 "模型"。独立工作的Jean-Pierre Queille和Joseph Sifakis提出了类似的想法。模型检查的技术诞生了。

模型检查方法的一大优势是，当它检测到系统设计中的问题时，检查器会打印出一个引起该问题的行动序列的例子。最初的设计总是会有一些细节上的错误。模型检查所提供的错误跟踪对设计者来说是非常有价值的，因为这些跟踪可以精确地定位问题的来源。

避免状态空间爆炸
尽管1981年的论文[2]证明了模型检查在原则上是可行的，但它在实际系统中的应用受到了严重的限制。最紧迫的限制是要搜索的状态的数量。早期的模型检查器需要明确计算程序可能承担的每一种可能的数值配置。例如，如果一个程序在一周的每一天计算气象站的雨量毫米，它将需要7个存储位置。每个位置都必须足够大，以容纳一天中预期的最大雨量。如果一天的最高雨量是1米，这个简单的程序将有1021个可能的状态，比可观察到的宇宙中的星星数量略少。早期的模型检查器必须验证这些状态中的每一个所需的属性都是真的。

实际规模的系统所操作的数据比上面的简单例子要多得多。可能状态的数量也在以爆炸性的速度增长。这种快速增长被称为状态空间爆炸。尽管早期的模型检查器证明了该技术对于小型系统是可行的，但它还没有准备好被广泛使用。

克拉克和他的学生肯-麦克米伦有一个基本的洞察力。状态空间爆炸是因为一个内存位置所能承担的状态数量要比该位置本身的大小大得多、多得多。内存位置是紧凑的，因为它编码了许多潜在的状态，但每次只包含一个。Clarke和McMillan观察到，这个过程可以反向应用：通过正确的编码，许多潜在的状态可以由一个单一的值来表示。McMillan从文献中找到了一种编码，它既能满足简明地编码多种状态的双重目标，又能允许有效地计算时间逻辑中的公式。

新的表示方法极大地减少了表示状态空间所需的存储量，反过来又减少了在实际规模的系统上运行模型检查器所需的时间。他们把这些新系统称为符号模型检查器。1995年，Clarke、McMillan及其同事用这种方法证明了IEEE计算机组件互连标准设计中的缺陷。在此之前，这类标准的可靠性只被非正式地分析过，许多罕见的情况没有被考虑，潜在的错误没有被发现。这是第一次对IEEE标准的每一种可能的情况都进行详尽的检查。

通过这样的改进，模型检查已经成为一项成熟的技术。它被英特尔和微软等公司广泛用于验证集成电路、计算机网络和软件的设计。模型检查器已被用于分析系统，其状态空间（10120）远远大于可观察到的宇宙中的原子数量（约1080）。它在验证为最近几代集成电路设计的软件方面变得特别重要，这些集成电路具有多个处理器同时运行的特点。模型检查已经大大改善了现代生活所依赖的系统的可靠性和安全性。

作者。泰德-柯克帕特里克