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 mathematical problem.

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
model checking
was to avoid
having humans
construct proofs.”

your specification, and often you can use that to find really subtle errors in design.

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 power states.

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
checking?

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.

Such as?

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 entire system.

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