Via the Geomblog, I have just learned that ACM has named Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis the winners of the 2007 A.M. Turing Award for their original and continuing research on model checking. You can read the ACM press release here. This is, of course, outstanding news for the concurrency-theory and the computer-aided-verification communities, and I am looking forward to inform my students about the motivations for this award next time I preach on the importance of temporal logics as specification formalisms in computer science and on model checking and implementation verification.
Normally, I feel that I would have to write a few more lines on model checking in a post like this, but, with a couple of upcoming deadlines, I am very glad to see that Ganesh Gopalakrishnan has done all the work for me on Suresh's blog :-) (Thanks to both of them!) Let me just add that the basic idea underlying model checking can be concisely and memorably summarized by means of an equation that I first saw stated in a set of slides for a talk delivered by Moshe Vardi:
model checking = graphs + logic + algorithms.
Indeed, in model checking we use automata of some kind---that is, (labelled) graphs---to represent (an abstraction of) the actual behaviour of computing systems, (temporal) logics to describe what properties we expect systems to afford, and we employ algorithms to check whether the automaton representing the behaviour of the system has the desired properties at the press of a button. (Alternatively, one can say that we check whether the automaton is a model of the formula describing the specification; hence the name model checking for this verification and validation technique.) As remarked by Ganesh in his perspective on model checking, model checking tools and techniques and now being increasingly used in many other areas apart from system verification and validation. Decision processes, reliability models, planning in AI, optimal scheduling, (on-line) model-based testing and analysis of GUIs are just a few areas of application of model checking. I expect that more will emerge in the near future.
I am particularly happy about this award because, as I hope I have convinced you with the short and oversimplified account above, model checking is an area of TCS where both volume A and volume B TCS play a fundamental role. Moreover, teams working on model checking have produced software tools that can be used to sneak in TCS ideas in first-year courses for CS and engineering students, thus awakening the students' interest in our beautiful area of scientific endeavour. What more can we ask for?
Congrats to Ed, Allen and Joseph!
Addendum (6 February 2008): Make sure you read Rance Cleaveland's guest post on the Complexity Weblog, and that you do not miss Paul Beame's very informative comment.
No comments:
Post a Comment