2007 E. 艾伦-艾默生

shiyi18

E. Allen Emerson

PHOTOGRAPHS
BIRTH:
2 June, 1954, Dallas,TX, USA

EDUCATION:
B.S. in Mathematics, University of Texas at Austin, (1976); Ph.D. in Applied Mathematics, Harvard University (1981).

EXPERIENCE:
Professor of Computer Science, University of Texas at Austin (from 1981).

HONORS AND AWARDS:
ACM Paris Kanellakis Theory and Practice Award, (1998); CMU Allen Newell Award for Research Excellence, (1999); IEEE Logic in Computer Science Test-of-Time Award (2006); ACM A. M. Turing Award (2007).


E. ALLEN EMERSON DL Author Profile link
United States – 2007
CITATION
Together with Edmund Clarke 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
VIDEO INTERVIEW
Life

E. Allen Emerson II was born and grew up in Dallas, Texas. He was always interested in scientific and mathematical topics. He taught himself calculus several years before he took it in public school. Emerson took a course on computer programming in high school, and learned BASIC on a GE Mark I Time Sharing System. Subsequently, he taught himself Fortran and Algol (from the Algol 60 report), and ran programs on a Burroughs B5500 mainframe computer.

Emerson studied as an undergraduate at the University of Texas in Austin, where he earned his B.S. in Mathematics in 1976. He went on to graduate school at Harvard University, obtaining a Ph.D. in Applied Mathematics (Computer Science) in 1981. Shortly thereafter he joined the University of Texas in Austin as a faculty member, and has remained there since. He is now Regents Chair and Professor of Computer Science.

Emerson discusses his decision to follow a career in computer science rather than mathematics.       
He has an interest in formal methods for establishing program correctness that dates back to his college days. This was inspired in part by reading a Communications of the ACM paper by Tony Hoare, "Proof of Program: Find". Also inspirational was a talk by Zohar Manna on fixpoints and the Tarski-Knaster Theorem given in the 1970's at the University of Texas. He was also intrigued by the work of J. W. De Bakker, W. P De Roever, and Edsger W. Dijkstra on predicate transformers.

Emerson discusses the origins of his interest in program verification and critiques approaches favored in the 1970s when he was in graduate school.       
The Model Checking Approach

Working in North America in the early 1980's, Emerson, in collaboration with Edmund Clarke, originated the technical concepts of an automated quality assurance method that checks if a nominally finite state concurrent system provides a model of (i.e., satisfies) its specification. They also coined the now ubiquitous term Model Checking for the method. Working in Europe, Joseph Sifakis independently discovered a similar idea. This model checking method had several desirable characteristics:

it was fully automatable and algorithmic, since it entailed a systematic search of the program's state space;
it was precise and expressive, with a formally defined specification logic, Computation Tree Logic (CTL), that could capture a wide variety of correctness properties of interest;
it was efficient, having running time that is polynomial in the sizes of both the input system and the specification, partly owing to this particular logic;
it was very appropriate for reasoning about concurrent programs, for which traditional quality assurance methods had proven largely ineffective;
it was conceived from the beginning to provide a practical basis for a practical verification method.
Emerson defines the model checking approach to hardware and software verification and discusses his development of the concept with Edmund Clarke.       
Emerson’s path-breaking contributions to the development of model checking include the formulation of widely used logics for flexible and expressive specifications as well as associated model checking algorithms. The expressiveness of powerful computation tree logics, as well as fixpoint logics are fundamental in both theory and practice. Arguably, expressiveness is even more basic than the efficiency for reasoning methods: if the important correctness properties cannot even be expressed, the logics are not useful for program verification. Much of the logical machinery developed by Emerson is central to most industrial specification logics and related model checking tools. As a result, the logics have been incorporated into several prominent commercial frameworks (e.g. IBM Sugar) and engineering standards for specification (e.g. Accellera-IEEE Property Specification Logic, IBM Property Specification Logic/Sugar).

The original paper [2] described the basic principles of model checking. However, it and all subsequent model checkers must contend with efficiency issues. Intuitively, the problem is that small programs can have an extremely large number of states, i.e. configurations of program variables including data values and location counters. Early model checkers typically computed every possible state of the program. This could lead to a combinatorial blowup in the size of the system state graph known by the term state explosion. For example, a concurrent system with 50 similar processes each having just 10 local states might have an astronomical 10**50 global states. As the field progressed, a number of powerful techniques were devised to ameliorate state explosion, often based on simplifying or shrinking the representation of the state graph. Consequently, the size of systems amenable to model checking has increased enormously over the years. While state explosion has not been completely vanquished, it has been largely tamed for many applications.

Avoiding Combinatorial Explosion

As the long version of the A.M. Turing Award citation noted, "The progression of Model Checking to the point where it can be successfully used for complex systems has required the development of sophisticated means of coping with what is known as the “state explosion problem”. Great strides have been made on this problem since 1981 by what is now a very large international research community. As a result, many major hardware and software companies are now using Model Checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms."

Emerson discusses the early adoption of model checking by industry and the challenges to its practical use caused by an explosion of states to evaluate.       
In most cases the system size dominates, and even the exponential blow-up for a small specification in linear temporal logic might be tolerable. But in other cases the specification is large, resulting in a substantial (exponential or worse) blow-up that is not workable. Emerson's work addresses efficiency in both the system size and the specification size. An advantage of using logics such as CTL is that the cost of model checking is linear in the size of the specification.

Emerson has also made highly innovative and influential advances in techniques for limiting state explosion. One technique exploits the redundancy that results from the symmetry inherent in systems comprised of many copies of similar sub-components. This allows large systems to be converted into much smaller systems, permitting dramatic increases in the speed and capacity of model checkers. Symmetry reduction permits reasoning about a large model using an exponentially reduced model. Many model checking tools incorporate symmetry reduction, including Rulebase from IBM. Emerson has also been a pioneer in combining reductions with other means of combating state explosion, such as symmetry reduction with symbolic model representations, or symmetry reduction with partial order reduction.

Another line of Emerson's work has been an examination of a key component of some model checking approaches. This involved applying fixpoint logics to check non-emptiness of automata on infinite objects and calculate winning strategies for games between an open system and its environment. These have applications to model checking multi-agent systems. Work at the Weizmann Institute similarly employed computation tree logics for automatic program design, and more recently for compositional reasoning.

Another approach solves many important cases of the parameterized model checking problem, where one must establish correctness for systems comprised of n sub-components, for all n. Emerson has used these techniques to algorithmically verify an unboundedly long automotive data protocol for Motorola, and to verify arbitrarily large systems of common cache protocols.

Emerson is an Highly Cited Researcher of the Information Sciences Institute, a recognition given to the 250 most referenced computer science researchers. He has served as editor for leading formal methods journals, including ACM Transactions on Computational Logic (ToCL), Formal Methods in Systems Design (FMSD), Formal Aspects of Computing (FAC), and Methods of Logic in Computer Science (MLCS). He is a founding member of the steering committee for the formal methods conference Automated Tools for Verification and Analysis (ATVA), and he serves on the steering committee of Verification, Model Checking, and Abstract Interpretation (VMCAI).

Author: Thomas Wahl



E. 艾伦-艾默生

照片
出生地
1954年6月2日，美国德克萨斯州达拉斯。

教育经历
德克萨斯大学奥斯汀分校数学学士（1976）；哈佛大学应用数学博士（1981）。

工作经验
德克萨斯大学奥斯汀分校计算机科学教授（1981年起）。

荣誉和奖项。
ACM巴黎卡内拉基斯理论与实践奖，（1998年）；CMU艾伦-纽维尔卓越研究奖，（1999年）；IEEE计算机科学逻辑测试时间奖（2006年）；ACM A. M. 图灵奖（2007年）。


E. ALLEN EMERSON DL作者简介链接
美国 - 2007年
参考文献
与Edmund Clarke和Joseph Sifakis一起，表彰他们在将模型检查发展为一种高效的验证技术方面所发挥的作用，该技术在硬件和软件行业被广泛采用。

简短注释
书目
亚马逊图灵奖
讲座视频
研究
题材
视频采访
生命

E. 艾伦-艾默生二世在德克萨斯州的达拉斯出生并长大。他一直对科学和数学课题感兴趣。他在公立学校学习微积分的几年前就自学了。艾默生在高中时选修了一门计算机编程课程，并在GE Mark I时间共享系统上学习BASIC。随后，他自学了Fortran和Algol（来自Algol 60报告），并在Burroughs B5500大型计算机上运行程序。

艾默生在奥斯汀的德克萨斯大学读本科，并于1976年获得数学学士学位。他继续在哈佛大学读研究生，于1981年获得应用数学（计算机科学）的博士学位。此后不久，他加入奥斯汀的德克萨斯大学成为一名教师，并一直在那里工作至今。他现在是执政者主席和计算机科学教授。

艾默生讨论了他决定从事计算机科学而不是数学的职业。       
他对建立程序正确性的正式方法感兴趣，这可以追溯到他的大学时代。这部分是受到阅读Tony Hoare的《ACM通讯》论文 "Proof of Program: 找到"。Zohar Manna在20世纪70年代在德克萨斯大学发表的关于fixpoints和Tarski-Knaster定理的演讲也给了他启发。他还对J. W. De Bakker、W. P. De Roever和Edsger W. Dijkstra关于谓词变换器的工作很感兴趣。

Emerson讨论了他对程序验证的兴趣的起源，并对他在读研究生时在20世纪70年代赞成的方法进行了批评。       
模型检查的方法

20世纪80年代初，Emerson在北美工作，与Edmund Clarke合作，提出了自动化质量保证方法的技术概念，即检查一个名义上的有限状态的并发系统是否提供了其规范的模型（即满足）。他们还为这种方法创造了现在无处不在的术语 "模型检查"。在欧洲工作时，Joseph Sifakis独立发现了一个类似的想法。这种模型检查方法有几个理想的特点。

它是完全自动化和算法化的，因为它需要对程序的状态空间进行系统的搜索。
它精确而富有表现力，有一个正式定义的规范逻辑，即计算树逻辑（CTL），可以捕捉各种感兴趣的正确性属性。
它是高效的，其运行时间与输入系统和规范的大小成多项式，部分原因在于这种特殊的逻辑。
它非常适用于对并发程序进行推理，而传统的质量保证方法在这方面已被证明是无效的。
它从一开始就被认为是为实用的验证方法提供了一个实用的基础。
Emerson定义了硬件和软件验证的模型检查方法，并讨论了他与Edmund Clarke对这一概念的发展。       
爱默生对模型检查的发展做出了开创性的贡献，包括为灵活和富有表现力的规范制定了广泛使用的逻辑学，以及相关的模型检查算法。强大的计算树逻辑的表现力，以及fixpoint逻辑在理论和实践上都是基本的。可以说，对于推理方法来说，可表达性甚至比效率更基本：如果重要的正确性属性甚至不能被表达，那么这些逻辑对于程序验证就没有用。由Emerson开发的许多逻辑机制是大多数工业规范逻辑和相关模型检查工具的核心。因此，这些逻辑已被纳入几个著名的商业框架（如IBM Sugar）和规范的工程标准（如Accellera-IEEE属性规范逻辑，IBM属性规范逻辑/Sugar）。

最初的论文[2]描述了模型检查的基本原则。然而，它和所有后续的模型检查器必须与效率问题作斗争。直观地说，问题在于小程序可以有非常多的状态，即程序变量的配置，包括数据值和位置计数器。早期的模型检查器通常计算程序的每一个可能的状态。这可能会导致系统状态图大小的组合爆炸，这就是所谓的状态爆炸。例如，一个有50个类似进程的并发系统，每个进程只有10个本地状态，可能有10**50个天文数字的全局状态。随着该领域的发展，一些强大的技术被设计出来以改善状态爆炸，通常是基于简化或缩小状态图的表示。因此，多年来，可用于模型检查的系统的规模已经大大增加。虽然状态爆炸还没有被完全消灭，但对于许多应用来说，它已经在很大程度上被驯服了。

避免组合爆炸

正如A.M.图灵奖引文的长版本所指出的，"模型检查发展到可以成功用于复杂系统的地步，需要开发出复杂的手段来应对所谓的 "状态爆炸问题"。自1981年以来，一个非常大的国际研究团体在这个问题上已经取得了巨大的进展。因此，许多主要的硬件和软件公司现在都在实践中使用模型检查。其使用的例子包括VLSI电路的验证、通信协议、软件设备驱动程序、实时嵌入式系统和安全算法"。

Emerson讨论了工业界对模型检查的早期采用，以及由于要评估的状态爆炸而对其实际使用造成的挑战。       
在大多数情况下，系统规模占主导地位，甚至线性时态逻辑中的小规范的指数爆炸可能是可以容忍的。但在其他情况下，规格很大，导致大量（指数或更大）的爆炸，这是不可行的。Emerson的工作同时解决了系统规模和规范规模的效率问题。使用诸如CTL这样的逻辑学的好处是，模型检查的成本与规范的大小呈线性关系。

艾默生还在限制状态爆炸的技术方面取得了高度创新和有影响力的进展。其中一项技术是利用了由许多类似子组件的副本组成的系统中固有的对称性所产生的冗余性。这使得大型系统可以被转换为更小的系统，从而使模型检查器的速度和能力得到极大的提高。对称性减少允许用指数级减少的模型来推理一个大模型。许多模型检查工具都包含了对称性还原，包括IBM的Rulebase。艾默生也是将还原与其他对抗状态爆炸的手段相结合的先驱，如对称性还原与符号模型表示，或对称性还原与偏序还原。

艾默生的另一项工作是对一些模型检查方法的关键部分进行研究。这涉及到应用火点逻辑来检查无限对象上的自动机的非emptiness，以及计算一个开放系统和其环境之间游戏的获胜策略。这些都可以应用于多Agent系统的模型检查。魏茨曼研究所的工作也同样采用了计算树逻辑来进行自动程序设计，最近则用于组合推理。

另一种方法解决了参数化模型检查问题的许多重要案例，在这些案例中，人们必须为由n个子组件组成的系统建立正确性，对于所有的n。

艾默生是信息科学研究所的高引用率研究人员，这是给予250名引用率最高的计算机科学研究人员的认可。他曾担任领先的形式化方法期刊的编辑，包括ACM Transactions on Computational Logic (ToCL), Formal Methods in Systems Design (FMSD), Formal Aspects of Computing (FAC), and Methods of Logic in Computer Science (MLCS)。他是形式化方法会议Automated Tools for Verification and Analysis (ATVA)的指导委员会的创始成员，并在Verification, Model Checking, and Abstract Interpretation (VMCAI)的指导委员会任职。

作者。Thomas Wahl