标题: 2007 E. 艾伦-艾默生 [打印本页] 作者: shiyi18 时间: 2022-4-17 23:10 标题: 2007 E. 艾伦-艾默生 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大型计算机上运行程序。
艾默生讨论了他决定从事计算机科学而不是数学的职业。
他对建立程序正确性的正式方法感兴趣，这可以追溯到他的大学时代。这部分是受到阅读Tony Hoare的《ACM通讯》论文 "Proof of Program: 找到"。Zohar Manna在20世纪70年代在德克萨斯大学发表的关于fixpoints和Tarski-Knaster定理的演讲也给了他启发。他还对J. W. De Bakker、W. P. De Roever和Edsger W. Dijkstra关于谓词变换器的工作很感兴趣。
艾默生是信息科学研究所的高引用率研究人员，这是给予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)的指导委员会任职。
