Model checking technology arguably ranges among the foremost applications of logic to computer science and computer engineering. In the twenty-five years since its invention, model checking has achieved multiple breakthroughs, bridging the gap between theoretical computer science, hardware and software engineering. Today, model checking is extensively used in the hardware industry, and has become feasible for verifying many types of software as well. Model checking has been introduced into computer science curricula at universities worldwide, and virtually has become a universal tool for the analysis of systems.

As the number of research groups and conferences in model checking is steadily increasing, the symposium will focus on the state of the art and the future challenges in model checking, seen through the eyes of the leading researchers which have shaped the field during the last decades.

The symposium will consist of invited lectures delivered by leading researchers in the field of model checking. The invited speakers are encouraged to reflect the state of the art in their respective field of expertise, and to focus on the most important and exciting future research directions.

Organizers / Editors

Orna Grumberg, Technion Haifa, Israel
Helmut Veith, Technische Universität München, Germany

List of speakers and short abstracts

Rajeev Alur, University of Pennsylvania
Model Checking: From Tools to Theory

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.

Randy Bryant, Carnegie Mellon University
A View from the Engine Room: Computational Support for Symbolic Model Checking

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-Putnam-Logemann-Loveland (DPLL) algorithm have greatly extended the reach of bounded model checkers.

OBDDs and DPLL-based checkers have very complementary strengths. OBDDs readily handle quantified Boolean formulas (QBF), whereas attempts to extend DPLL to QBF have had limited success. Some SAT problems that are completely intractable for DPLL 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 DPLL. A successful hybrid of these two would have profound impact on symbolic model checking.

Edmund Clarke, Carnegie Mellon University
Model Checking: My 25 year quest to overcome the state-explosion problem

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.

David Dill, Stanford University
A retrospective on Murphi

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.

E Allen Emerson, University of Texas, Austin
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.

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

Krishnendu Chatterjee and Thomas Henzinger, EPFL Lausanne and UC Berkeley
From Graph Models to Game Models

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.

Gerard Holzmann, NASA/JPL
Complexity, Abstraction, and Software Model Checking

The ultimate application for model checking is in the thorough verification of the behavior of asynchronous software systems. Ideally, model checking is applied to higher level models of a software system, but sometimes all that is available is the implementation artifact. Manually constructed models are rarely available and rarely accurate for very long, which can make verification results suspect. Implementation level code, on the other hand, often has too much detail, which can make verification impossible.
Abstraction plays a key role in addressing both issues. I will discuss the progress we've made in this domain to date and what we hope to achieve in the coming years.

Bob Kurshan, Cadence Berkeley
25 Years of Computer-Aided Verification

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".

Ken McMillan, Cadence Berkeley
The Evolution of Symbolic Model Checking

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.

Amir Pnueli, Weizmann Institute and New York University
The Merits of Temporal Observers

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.

Moshe Y. Vardi, Rice University, Houston
From Prior to PSL

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.