| 25MC | 25 Years of Model Checking Seattle, August 16, 2006 |
25MC on Wednesday, August 16th
Session (09:00‑10:30)
| 09:00‑09:30 | Edmund Clarke
(Carnegie Mellon University) The Birth of Model Checking [ppt] The most important problem in Model Checking is the State-Explosion Problem. In particular, it is far more important than the logic or specification formalism that is used -- CTL, LTL, CTL*, Buchi Automata, or the mu-calculus. Since Allen Emerson and I first proposed that Model Checking could be used for verification of finite state systems in 1981, most of my research has focused on this problem. Model Checking has abysmal complexity in worst case as a function of word size or number of processes, and most theoreticians were very pessimistic at first. However, by using techniques that exploit abstraction, symmetry, compositional reasoning, the partial order reduction, parameterized designs, OBDDs, propositional satisfiability, and counterexample-guided abstraction refinement (CEGAR), we are often able to handle surprisingly large examples. I will survey the progress that we have made with emphasis on my research and that of my students. I will also speculate on where we may be able to make progress in the future. |
| 09:30‑10:00 | E. Allen Emerson
(University of Texas, Austin) The Beginnings of Model Checking: A Personal Perspective Model checking realizes in small part the Dream of Leibniz to permit calculation of the truth of formalized assertions. Despite being hampered by state explosion, over the past 25 years model checking has had a substantive impact on program verification efforts: going from discussions of how to manually prove programs correct to the routine, automated, model-theoretic verification of many programs in industrial practice. We will discuss the mathematical and pragmatic themes underlying this development, and then go on to make some forecasts as to what might be needed in the future. |
| 10:00‑10:30 | Bob Kurshan (Cadence Berkeley) 25 Years of Computer-Aided Verification [pdf] I will trace the evolution of the title subject from the laboratory to the marketplace, following a variety of technologies over the daunting hurdles of "technology transfer". |
Break (10:30‑11:00)
Session (11:00‑12:30)
| 11:00‑11:30 | Gerard Holzmann
(NASA/JPL) New Challenges in Model Checking [pdf] In the last 25 years, the notion of performing software verification with logic model checking techniques has evolved from intellectual curiosity to accepted technology with significant potential for broad practical application. In this talk we look back at the main steps in this evolution and illustrate how the challenges have changed over the years, as we sharpened our theories and tools. Next we discuss a typical challenge in software verification that we face today – and that perhaps we can look back on in another 25 years as having inspired the next logical step towards a broader integration of model checking into the software development process. This is a joint work with Rajeev Joshi and Alex Groce. |
| 11:30‑12:00 | David Dill
(Stanford University) A Retrospective on Murphi [ppt] Murphi is an explicit-state model checker for safety properties. It has been widely used in academia and industry, especially for multiprocessor cache coherence protocols. The success of Murphi in its "ecological niche" is due to several research innovations as well as some good engineering decisions. This talk will review the history of the development of the tool, some of the interesting ideas in it, problems to which it has been applied, and the ad hoc and somewhat random path that lead to a working tool. |
| 12:00‑12:30 | Rajeev Alur
(University of Pennsylvania) Model Checking: From Tools to Theory [ppt] Model checking is often cited as a success story for transitioning and engineering ideas rooted in logics and automata to practice. In this talk, we will discuss how the efforts aimed at improving the scope and effectiveness of model checking tools have revived the study of logics and automata leading to unexpected theoretical advances whose impact is not limited to model checking. We will illustrate this with sample results in tree automata, context-free languages, and timed automata, and resulting new insights in fields such as databases and control theory. |
25MC Lunch/Panel (12:30‑14:00)
Chair:
Orna Grumberg
Session (14:00‑15:30)
| 14:00‑14:30 | Thomas Henzinger
(EPFL Lausanne & UC Berkeley) From Graph Models to Game Models [ppt] A model that preserves the individuality of multiple actors in a transition system is a game model. The resulting game is played on the state space of the system. The players represent different processes of the system, or the environment. In a given state, the choices made by the players determine the successor state. Some of the players may compete, others collaborate, with the objective of satisfying a temporal specification. A graph model (or Kripke structure) is the special case of a game model where there is only a single player (who resolves nondeterminism). Game solving, therefore, is the generalization of model checking to two or more players. Game models are necessary to ask and answer certain important questions about systems. In particular, the problem of synthesizing a reactive system that satisfies a temporal specification is a problem of constructing a winning strategy. Other applications include compatibility checking for components, receptiveness and refinement checking for models, and test-case generation. Moreover, game models offer the flexibility to limit the knowledge of a player when making a choice, to allow a player probabilistic choices, and to combine the choices of different players in synchronous or asynchronous fashion. The precise formalization of a game will determine the difficulty of solving it. We survey classical and recent results on games with omega-regular winning conditions, as well as their applications in system design and verification. |
| 14:30‑15:00 | Limor Fix
(Intel Pittsburgh) Accelerating the Industrial Deployment of Model-Checking for SW Verification: Lessons from 10 years of Model-Checking Deployment for HW Verification in Intel [ppt] Model checking technologies have been applied to hardware verification in the last 15 years. Pioneering work has been conducted by Intel since 1990 using model checking technologies to build industrial hardware verification systems. This talk will review the evolution and the success of these systems in Intel and in particular it will focus on the many challenges and learning that have resulted from changing how hardware validation is performed in Intel to include formal verification. The talk will also include a discussing of how the learning from hardware verification can be used to accelerate the industrial deployment of model-checking technologies for software verification. |
| 15:00‑15:30 | Randy Bryant
(Carnegie Mellon University) A View from the Engine Room: Computational Support for Symbolic Model Checking [ppt] Symbolic model checking arose from the marriage of a Boolean-level representation of the model-checking task with a computational engine that supported the required set of operations. Ordered Binary Decision Diagrams (OBDDs) were the first approach with the necessary combination of efficiency and expressive power. More recently, Boolean satisfiability (SAT) checkers based on the Davis-Logeman-Loveland (DLL) algorithm have greatly extended the reach of bounded model checkers. OBDDs and DLL-based checkers have very complementary strengths. OBDDs readily handle quantified Boolean formulas (QBF), whereas attempts to extend DLL to QBF have had limited success. Some SAT problems that are completely intractable for DLL are quite trivial with OBDDs. On the other hand, OBDDs cannot cope with problems that involve large numbers of variables, whereas SAT checkers are relatively insensitive to the number of variables. Despite many attempts, no one has found a way to combine the bottom-up approach of OBDDs with the top-down approach of DLL. A successful hybrid of these two would have profound impact on symbolic model checking. |
Break (15:30‑16:00)
Session (16:00‑17:30)
| 16:00‑16:30 | Ken McMillan
(Cadence Berkeley) The Evolution of Symbolic Model Checking [ppt] This talk will trace the evolution of symbolic model checking over nearly two decades. We will note several general trends. In the early years the emphasisis was on increasingly sophisticated representations and image computation methods. This includes various generalizations, such as regular model checking, and a proliferation of methods for Boolean quantifier elimination. More recently, the trend has been toward approximate fixed point computations, which in effect allow us to prove weaker properties of larger systems. This has resulted in a synthesis of symbolic model checking and abstract interpretation. Still, given all this progress it is surprising to find BDD-based symbolic model checking at the heart of many modern systems. |
| 16:30‑17:00 | Moshe Y. Vardi
(Rice University, Houston) From Church and Prior to PSL [pdf] One of the surprising deveopments in the area of program verification is how ideas introduced originally by Prior in the 1950s ended up yielding by 2004 an industrial-standard property-specification language called PSL. This development was enabled by the equally unlikely transformation of mathematical machinery, inroduced by Buechi in the early 1960 for second-order number theory, into effective algorithms for model checking tools. This talk will attempt to depict the tangled skein of this development. |
| 17:00‑17:30 | Amir Pnueli
(Weizmann Institute and New York University) The Merits of Temporal Testers: Transducers Compose while Acceptors Do Not [pdf] A central component in model checking temporal properties of finite-state systems is the translation of an LTL formula into a finite-state Omega automaton. According to the standard translation, automaton A corresponds to LTL formula f if the set of sequences accepted by A is precisely the set of sequences that satisfy f. This implies that the correspondence between A and f is required only at the initial position of each sequence. In this talk we consider a stronger notion of translation, in which the automaton A_f, called the TEMPORAL OBSERVER of formula f, has a Boolean output variable x such that x=1 at position j of a sequence s iff (s,j) |= f. We will describe several advantages of the temporal observer construct. The construction of temporal observers is modular. That is, the temporal observer of a formula "f op g", where "op" can be any Boolean or temporal operator applied to arbitrary LTL formulas f and g, can be constructed by combining the temporal observers of f, g, and "op". As a result, we can outline a model-checking algorithm for LTL formulas which is compositional in the structure of the formula. This type of compositionality has been long considered to be a unique feature of CTL. Based on this approach to LTL model checking, we will present a compositional method for model-checking arbitrary CTL* formulas. We will show how the notion of temporal testers is easily and naturally extended to deal with past formulas and many of the new operators introduced in the new hardware property specification language PSL. It can also be adapted to deal with versions of LTL which are evaluated over finite sequences as well as infinite sequences, as is often required in applications of testing and run-time verification. |
