25 Years of Model Checking Symposium
Affiliated to CAV 2006
August 16, 2006, FLOC 2006, Seattle
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
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,
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,
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,
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
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,
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,
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
- 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.