tag:blogger.com,1999:blog-3722233.post5540189807646496684..comments2024-03-02T02:08:38.816-06:00Comments on Computational Complexity: This years Turing Award: Model CheckingLance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-3722233.post-8538310869407031982008-02-10T03:34:00.000-06:002008-02-10T03:34:00.000-06:00I'm very happy to see the Turing go to model check...I'm very happy to see the Turing go to model checking. That was one of the areas I felt should have been given preference over the previous two Yet Another Compiler Writer awards (of which I consider the Naur one to be an obvious mistake at this point in time -- he should have gotten it (very) early on or not at all because so many others have contributed more since, including some in his own department).<BR/><BR/>I thought that Gerard Holzman would be one of the recipients if the Turing was ever awarded for model checking but he was left out. That surprises me.<BR/><BR/>(Others that I think would have been preferable to Naur and possibly Allen: Scheifler and Gettys for X, Miller, Clifford, and Kohl for Kerberos.)Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-4773987969000496212008-02-07T03:24:00.000-06:002008-02-07T03:24:00.000-06:00Model checking is widely used in hardware but mode...Model checking is widely used in hardware but model checking techniques are also considered very valuable in practice on aspects of software. (One example in the SLAM project at Microsoft for verifying device drivers.) A great aspect is how much theory has been involved in making this successful. (One theorem about automata due to Buchi that I mention below deserves to be more widely known and allows one to verify pushdown systems and not just finite automata!)<BR/><BR/>The award winners deserve a huge amount of credit for realizing that model checking was the way to go and championing it over more than a decade before it really caught on. It is hard to get a sense of how far from practical this approach was considered in the early 1980's. After all the problem they wanted to solve is a generalization of deciding graph reachability in an exponential size but polynomially-specified graph. <BR/><BR/>The success of model checking owes much to theoretical ideas that have advanced the state of the art in a big way. These include the ideas of Vardi and Wolper (Godel prize a few years ago) who derived new efficient algorithms for automata-theoretic verification that were later incorporated and extend by Kurshan and Holzmann (along with refinements by others) in the SPIN model checker (for which the four won the Kannelakis prize). See Kurshan's 1994 STOC invited talk for an overview of the approach.<BR/><BR/>A huge advance was symbolic model checking using BDDs (oblivious read-once branching programs championed as a data structure for Boolean functions by Randy Bryant) developed in Ken McMillan's ACM Award-winning dissertation in the early 1990's. (Kannelakis Award for Bryant, Clarke, Emerson, and McMillan.)<BR/><BR/>In the late 1990's improvements in SAT solvers made them efficient enough to replace BDDs for bounded model checking. <BR/><BR/>All three of these approaches have domains in which they are preferred.<BR/><BR/>Subsequent to this line of work there has been a huge flowering of different ideas for verifying aspects of software. One major idea has been abstraction-refinement in which one abstracts away most of the detail of the software in the initial model and then adds detail automatically based on how verification fails and then tries again. (Interpolation results about resolution proofs actually can be useful here.)<BR/><BR/>The most surprising aspect from my point of view, though maybe not the most important, has been the ability to verify pushdown systems. Verifying these is obviously necessary to handle the call stack. How can one possibly use finite state verification to determine properties of pushdown automata? <BR/><BR/>Buchi's theorem I mentioned above does this:<BR/>For any PDA M with stack alphabet Gamma, the language S(M) over Gamma^* of consisting of all possible stack configurations of M is regular! Moreover, given M one can build an NFA for S(M) fairly efficiently. (Actually one works with a language in Q Gamma^* that includes the state in the configuration.) So, for example, in order to verify a safety property (one that is always true) one can work with a verification that involves finite automata only!<BR/><BR/>This property of stack languages seems like such a natural one that it would be described in standard textbooks. (Consider how simple the possible stacks are for any of the familiar PDAs you know.) What is the simplest proof that anyone can come up with?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-15871918781780605512008-02-06T17:35:00.000-06:002008-02-06T17:35:00.000-06:00thank you for a instructive guest-post!it sounds l...thank you for a instructive guest-post!<BR/><BR/>it sounds like symbolic model checking is used for hardware verification, is it practical for software verification anymore?Anonymousnoreply@blogger.com