The 2009 Visions of Computing Lecture: Model Checking Over Time


 Model Checking Over Time

 Model Checking Over Time

 

March 2 , 2009 from 4:15 p.m. - 5:30 p.m. Lecture in Avaya Auditorium, ACES 2.302; private reception for invited guests followed from 5:45 p.m. - 7:30 p.m.

The Visions of Computing Lecture Series highlights faculty accomplishments and provides public education about computer science.

4:15 - 4:30
Welcome - UTCS Chair, J Strother Moore

4:30 – 5:30
Turing Address - E. Allen Emerson/UTCS Faculty and Turing Award Winner

5:45 – 7:30
Reception for invited guests

About Dr. Emerson

Bio:

Dr. Emerson is Regents Chair and Professor in Computer Sciences at the University of Texas at Austin. Emerson works in formal methods for verifying and debugging programs, and is co-founder of the successful field of model checking for automatically verifying correctness of nominally finite state systems. In recognition of this achievement, Emerson is a recipient of the 2007 ACM Turing Award. Emerson is also a recipient of the ACM Kanellakis Theory and Practice Award for the invention of symbolic model checking, and the 2006 IEEE Logic in Computer Science Test-of-Time Award for contributions to logics of programs. Emerson serves on the editorial boards of major formal methods journals including Formal Methods in Systems Design and Formal Aspects of Computing. He also serves on the Steering Committees of the Verification, Model Checking, and Abstract Interpretation (VMCAI) Conference as well as the Automated Technology for Verification and Analysis (ATVA) Conference. Dr. Emerson received his BS in mathematics from the University of Texas at Austin and his PhD in applied mathematics from Harvard University.

ACM Turing Award Honors Founders of Automatic Verification Technology That Enables Faster, More Reliable Designs

NEW YORK, February 4, 2008 - ACM, the Association for Computing Machinery, has named Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis the winners of the 2007 A.M. Turing Award, widely considered the most prestigious award in computing, for their original and continuing research in a quality assurance process known as Model Checking. Their innovations transformed this approach from a theoretical technique to a highly effective verification technology that enables computer hardware and software engineers to find errors efficiently in complex system designs. This transformation has resulted in increased assurance that the systems perform as intended by the designers. Clarke, Emerson, and Sifakis developed this fully automated approach that is now the most widely used verification method in the hardware and software industries.

ACM President Stuart Feldman said the work of Clarke, Emerson and Sifakis has had a major impact on designers and manufacturers of semiconductor chips. "These industries face a technology explosion in which products of unprecedented complexity have to operate as expected for companies to survive. This verification advance enabled these industries to shorten time to market and increase product integrity. Without the conceptual breakthrough pioneered by these researchers, we might still be stuck with chips that have many errors and would lack the power and speed of today's equipment. This is a great example of an industry-transforming technology arising from highly theoretical research," Feldman said.

Citation

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.

About the A.M. Turing Award

The A.M. Turing Award was named for Alan M. Turing, the British mathematician who articulated the mathematical foundation and limits of computing, and who was a key contributor to the Allied cryptanalysis of the German Enigma cipher during World War II. Since its inception in 1966, the Turing Award has honored the computer scientists and engineers who created the systems and underlying theoretical foundations that have propelled the information technology industry. The Turing Award is considered the most prestigious award in computer science. It carries a $250,000 cash prize. The Turing Award is widely viewed as the "Nobel Prize" of computer science. For additional information see CACM, July 2008, p. 112.

Details at:

1. Parking
2. Map

Comments

Post new comment

The content of this field is kept private and will not be shown publicly.

Comments are moderated. They will be posted if they stick to the topic and contribute to the conversation. They will not be published if they contain or link to abusive material, personal attacks, profanity or spam.