on the data being exchanged in the
critical sections. Many communication
protocols had the same property. We
decided to see if we could analyze finite-state programs by algorithmic means.
How exactly does that work?
eae You have a program described by
its text and its specification described
by its text in some logic. It’s either true
or false that the program satisfies the
specification, and one wants to determine that.
JoSePh SifaKiS Right. You build a
mathematical model [of the program],
and on this model, you check some
properties, which are also mathematically specified. To check the property,
you need a model-checking algorithm
that takes as input the mathematical
model you’ve constructed and then
gives an answer: “yes,” “no,” or “I don’t
know.” If the property is not verified,
you get diagnostics.
And to formalize those specifica-
tions, those properties…
eae What people really want is the
program they desire, an inherently pre-formal notion. They have some vague
idea about what sort of program they
want, or perhaps they have some sort
of committee that came up with an
English prose description of what they
want the program to do, but it’s not a
So one benefit of model checking
is that it forces you to precisely specify
your design requirements.
emc Yes. But for many people, the
most important benefit is that if the
specification isn’t satisfied, the model
checker provides a counterexample
execution trace. In other words, it provides a trace that shows you exactly
how you get to an error that invalidates
“the idea behind
was to avoid
your specification, and often you can
use that to find really subtle errors in
How have model-checking algo-
rithms evolved over the years?
emc Model-checking algorithms
have evolved significantly over the past
27 years. The first algorithm for model
checking, developed by Allen and myself, and independently by Queille
and Sifakis, was a fixpoint algorithm,
and running time increased with the
square of the number of states. I doubt
if it could have handled a system with
a thousand states. The first implementation, the EMC Model Checker
(EMC stands for “Extended Model
Checker”), was based on efficient
graph algorithms, developed together
with Allen and Prasad Sistla, another
student of mine, and achieved linear
time complexity in the size of the state
space. We were able to verify designs
with about 40,000 states. Because of
the state-explosion problem, this was
not sufficient in many cases; we were
still not able to handle industrial designs. My student Ken McMillan then
proposed a much more powerful technique called symbolic model checking.
We were able to check some examples
with 10 to the one-hundredth power
states ( 1 with a hundred zeros after it).
This was a dramatic breakthrough but
was still unable to handle the state-explosion problem in many cases. In the
late 1990s, my group developed a technique called bounded model checking, which enabled us to find errors
in many designs with 10 to the 10,000
eae These advances document the
basic contribution of model checking.
For the first time, industrial designs
are being verified on a routine basis.
Organizations, such as IBM, Intel, Microsoft, and NASA, have key applications where model checking is useful.
Moreover, there is now a large model-checking community, including
model-checking users and researchers
contributing to the advance of model-checking technology.
What are the limitations of model
JS You have two basic problems:
how to build a mathematical model
of the system and then how to check a
property, a requirement, on that mathematical model.
First of all, it can be very challenging to construct faithful mathematical
models of complex systems. For hardware, it’s relatively easy to extract mathematical models, and we’ve made a lot
of progress. For software, the problem
is quite a bit more difficult. It depends
on how the software is written, but we
can verify a lot of complex software.
But for systems consisting of software
running on hardware, we don’t know
how to construct faithful mathematical models for their verification.
The other limitation is in the complexity of the checking algorithm, and
here we have a problem called the
state-explosion problem (that Clarke
referred to earlier), which means that
the number of the states may go exponentially high with the number of components of the system.
emc Software verification is a Grand
Challenge. By combining model checking with static analysis techniques, it
is possible to find errors but not give
a correctness proof. As for the state-explosion problem, depending on the
logic and model of computation, you
can prove theoretically that it is inevitable. But we’ve developed a number of
techniques to deal with it.
emc The most important technique
is abstraction. The basic idea is that
part of the program or the protocol
you’re verifying doesn’t really have any
effect on the particular properties that
you’re checking. So what you can do is
simply eliminate those particular parts
from the design.
You can also combine model checking with compositional reasoning,
where you take a complex design and
break it up into smaller components.
Then you check those smaller components to deduce the correctness of the
How large are the programs we can
currently verify with model checking?
emc Well, first of all, there’s not
always a natural correspondence between a program’s size and its complexity. But I would say we can often
check circuits with around 10 to the
100th power states ( 1 with a hundred
zeros after it).
JS Right. We know how to verify systems of medium complexity today—
it’s difficult to say but perhaps a program of around 10,000 lines. But we