ACM, the Association for Computing Machinery, has named Barbara Liskov of the Massachusetts Institute of Technology (MIT) the winner of the 2008 ACM A.M. Turing Award. The award cites Liskov for her foundational innovations to designing and building the pervasive computer system designs that power daily life. Her achievements in programming language design have made software more reliable and easier to maintain. They are now the basis of every important programming language since 1975, including Ada, C++, Java, and C#. The Turing Award, widely considered the "Nobel Prize in Computing," is named for the British mathematician Alan M. Turing. The award carries a $250,000 prize, with financial support provided by Intel Corporation and Google Inc.
The first U.S. woman to be awarded a Ph.D. from a computer science department (in 1968 from Stanford University), Liskov revolutionized the programming field with groundbreaking research that underpins virtually every modern computer application for both consumers and businesses. Her contributions have led to fundamental changes in building the computer software programs that form the infrastructure of our information-based society. Her legacy has made software systems more accessible, reliable, and secure 24/7.
Showing posts with label turing. Show all posts
Showing posts with label turing. Show all posts
Tuesday, March 10, 2009
Barbara Liskov wins the Turing Award
Via MM comes this news:
Monday, February 04, 2008
2007 ACM Turing Award, and a perspective on model checking.
The 2007 Turing Award was awarded to Edmund Clarke, E. Allen Emerson and Joseph Sifakis for their work on model checking. In our "theory A" cocoon, we tend not to pay attention to much "theory B" work, and model checking is one of the shining stars in theory B, with a rich theory and immense practical value.
I am not competent to discuss model checking at any level, and so I asked someone who is ! Ganesh Gopalakrishnan is a colleague of mine at the U. and heads our Formal Verification group. I asked him if he could write a perspective on model checking, and he kindly agreed. What follows is his piece (with URLs added by me). As usual, all credit to him, and any mistakes in transcribing are my fault alone.
A Perspective On Model Checking
Ganesh Gopalakrishnan
One of the earliest attempts at proving the correctness of a program was by Alan Turing in 1949. The activity was raised to a much more prominent level of interest and importance through the works of Dijkstra, Hoare, and others. Yet, the enterprise of "Program Verification" was met with more noticeable failures than successes in the 1970's, due to its inability to make a dent on practice. The introduction of Temporal Logic for modeling concurrent systems (for which Amir Pnueli won the 1996 Turing Award) was the first attempt at shifting the attention away from the impossibly difficult task of 'whole program verification' to a much more tractable focus on verifying the reactive aspects of concurrency.
Looking back, this enterprise did not meet with the expected degree of success, as Temporal Logic reasoning was still based on `deduction' (proof from first principles). From an engineer's perspective, what was needed was a simple way to specify the classes of "legal and illegal waveforms" a system can produce on its signals / variables, and an efficient way of checking that all those waveforms are contained in the set of "legal waveforms" as can be specified through temporal properties. In other words, it was sufficient to show that finite state machines (or finite state control skeletons of programs) served as *models* for a catalog of desired temporal properties.
This was essentially the approach of model checking. It immediately took off as a practically viable method for debugging concurrent systems; the approach guaranteed exhaustive verification for small instances of a problem. In practice it meant that all relevant corner cases were considered in the confines of afforable resource budgets. This was the gist of Allen Emerson's contribution in his PhD dissertation which he wrote under Ed Clarke's guidance. A parallel effort underway at France in Joseph Sifakis's group also arrived at the same pragmatic approach to verification. Model checking was given crucial impetus by Ken McMillan who, using the technology of Binary Decision Diagrams formulated and popularized by Randy Bryant, developed the highly efficient Symbolic Model Checking approach. The technology has since then skyrocketed in its adoption rate.
Today, model checking and its derivatives are part of every verification tool used to debug digital hardware. While "full verification" is not the goal (and is largely a meaningless term), the ability of model checkers to find *high quality bugs* is uncanny. It is those bugs that escape simulation, and may not even manifest in hardware that operates at the rate of GHz. Some of the error traces produced by model checkers are only about two dozen steps long; yet, if one imagines the number of reachable nodes in a tree with arity (branching factor) 2000 in two dozen steps, one understands why conventional approaches to testing miss bugs: they have to make the same lucky "1 in 2000" choices two dozen times in a row. A model checker can often get away by not really modeling these choices explicitly. Reduction techniques allow model checkers to detect and avoid exploring many "equivalent" behaviors. In that sense, model checking is one of the most powerful "test acceleration technologies" that mankind has invented.
Today, microprocessor companies employ several kinds of model checkers. In software, Bell Labs (mainly before its collapse), JPL, NASA, and Microsoft (to name a few) have had tremendous success using model checking for verifying device drivers, switch software, and flight control software. Speaking more generally, anything with a finite state structure (e.g., decision processes, reliability models, planning in AI) can be approached through model checking.
Aftermatter:
I am not competent to discuss model checking at any level, and so I asked someone who is ! Ganesh Gopalakrishnan is a colleague of mine at the U. and heads our Formal Verification group. I asked him if he could write a perspective on model checking, and he kindly agreed. What follows is his piece (with URLs added by me). As usual, all credit to him, and any mistakes in transcribing are my fault alone.
A Perspective On Model Checking
Ganesh Gopalakrishnan
One of the earliest attempts at proving the correctness of a program was by Alan Turing in 1949. The activity was raised to a much more prominent level of interest and importance through the works of Dijkstra, Hoare, and others. Yet, the enterprise of "Program Verification" was met with more noticeable failures than successes in the 1970's, due to its inability to make a dent on practice. The introduction of Temporal Logic for modeling concurrent systems (for which Amir Pnueli won the 1996 Turing Award) was the first attempt at shifting the attention away from the impossibly difficult task of 'whole program verification' to a much more tractable focus on verifying the reactive aspects of concurrency.
Looking back, this enterprise did not meet with the expected degree of success, as Temporal Logic reasoning was still based on `deduction' (proof from first principles). From an engineer's perspective, what was needed was a simple way to specify the classes of "legal and illegal waveforms" a system can produce on its signals / variables, and an efficient way of checking that all those waveforms are contained in the set of "legal waveforms" as can be specified through temporal properties. In other words, it was sufficient to show that finite state machines (or finite state control skeletons of programs) served as *models* for a catalog of desired temporal properties.
This was essentially the approach of model checking. It immediately took off as a practically viable method for debugging concurrent systems; the approach guaranteed exhaustive verification for small instances of a problem. In practice it meant that all relevant corner cases were considered in the confines of afforable resource budgets. This was the gist of Allen Emerson's contribution in his PhD dissertation which he wrote under Ed Clarke's guidance. A parallel effort underway at France in Joseph Sifakis's group also arrived at the same pragmatic approach to verification. Model checking was given crucial impetus by Ken McMillan who, using the technology of Binary Decision Diagrams formulated and popularized by Randy Bryant, developed the highly efficient Symbolic Model Checking approach. The technology has since then skyrocketed in its adoption rate.
Today, model checking and its derivatives are part of every verification tool used to debug digital hardware. While "full verification" is not the goal (and is largely a meaningless term), the ability of model checkers to find *high quality bugs* is uncanny. It is those bugs that escape simulation, and may not even manifest in hardware that operates at the rate of GHz. Some of the error traces produced by model checkers are only about two dozen steps long; yet, if one imagines the number of reachable nodes in a tree with arity (branching factor) 2000 in two dozen steps, one understands why conventional approaches to testing miss bugs: they have to make the same lucky "1 in 2000" choices two dozen times in a row. A model checker can often get away by not really modeling these choices explicitly. Reduction techniques allow model checkers to detect and avoid exploring many "equivalent" behaviors. In that sense, model checking is one of the most powerful "test acceleration technologies" that mankind has invented.
Today, microprocessor companies employ several kinds of model checkers. In software, Bell Labs (mainly before its collapse), JPL, NASA, and Microsoft (to name a few) have had tremendous success using model checking for verifying device drivers, switch software, and flight control software. Speaking more generally, anything with a finite state structure (e.g., decision processes, reliability models, planning in AI) can be approached through model checking.
Aftermatter:
- Daniel Jackson (MIT), "With its dramatic successes in automatically detecting design errors (mainly in hardware and protocols), model checking has recently rescued the reputation of formal methods." (source)
- "Proofs of programs are too boring for the social process of mathematics to work." DeMillo et al in CACM 1979).
Subscribe to:
Posts (Atom)