博文
A. M. Turing Award - 2007
||
伟大贡献:For his role in developing Model-Checking into a highly effective verification technology, widely adopted in the hardware and software industries.
具体情况：
In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly successful field of Model Checking. This verification technology provides an algorithmic means of determining whether an abstract model--representing, for example, a hardware or software design--satisfies a formal specification expressed as a temporal logic formula. Moreover, if the property does not hold, the method identifies a counterexample execution that shows the source of the problem. 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 over the past 27 years 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.
ACM President Stuart Feldman, Alan Eustace (Senior VP of Engineering and Research, Google), Andrew Chien (Vice President of Corporate Technology Group, Intel, and Director of Intel Research), Edmund Clarke, E. Allen Emerson, Joseph Sifakis, and ACM CEO John White at the 2008 ACM Awards Banquet.
原文地址 http://acm.org
https://blog.sciencenet.cn/blog-89075-43283.html
上一篇：Formal Methods Europe (FME)
下一篇：The Philosophy of Computer Science
具体情况：
In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly successful field of Model Checking. This verification technology provides an algorithmic means of determining whether an abstract model--representing, for example, a hardware or software design--satisfies a formal specification expressed as a temporal logic formula. Moreover, if the property does not hold, the method identifies a counterexample execution that shows the source of the problem. 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 over the past 27 years 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.
The work of Drs. Clarke, Emerson, and Sifakis continues to be central to the success of this research area. Their work over the years has led to the creation of new logics for specification, new verification algorithms, and surprising theoretical results. Model Checking tools, created by both academic and industrial teams, have resulted in an entirely novel approach to verification and test case generation. This approach, for example, often enables engineers in the electronics industry to design complex systems with considerable assurance regarding the correctness of their initial designs.
Edmund M Clarke
E Allen Emerson
Joseph Sifakis
ACM President Stuart Feldman, Alan Eustace (Senior VP of Engineering and Research, Google), Andrew Chien (Vice President of Corporate Technology Group, Intel, and Director of Intel Research), Edmund Clarke, E. Allen Emerson, Joseph Sifakis, and ACM CEO John White at the 2008 ACM Awards Banquet.
原文地址 http://acm.org
https://blog.sciencenet.cn/blog-89075-43283.html
上一篇：Formal Methods Europe (FME)
下一篇：The Philosophy of Computer Science
