A conversation with the 2007 ACM A.M. Turing Award winners.
EDMUND M. ClARkE, E. Allen
Emerson, and Joseph Sifakis
were honored for their role in
into a highly effective verification technology, widely adopted in
the hardware and software industries.
Let’s talk about the history of formal
e. aLLen emeRSon By the late 1960s,
we recognized that a program should
be viewed as a mathemat ical object.
It has a syntax and semantics and formally defined behavior engendered by
that syntax and semantics. The idea
was to give a mathematical proof that
a program met a certain correctness
specification. So one would have some
axioms characterizing the way the program worked for such-and-such an
instruction and some inference rules,
and one would construct a formal
proof of the system, like philosophers
But it never really seemed to scale up
to large programs. You ended up with
something like 15-page papers proving
that a half-page program was correct. It
was a great idea but didn’t seem to pan
out in practice.
What about the history of model
eDmunD m. cLaRKe The birth of model
checking was quite painful at times.
Like most research on the boundary between theory and practice, theoreticians
thought the idea was trivial, and system
builders thought it was too theoretical.
Researchers in formal methods were
even less receptive. Research in the for-
mal-methods community in the 1980s
usually consisted of designing and
verifying tricky programs with fewer
than 50 lines using only pen and paper.
If anyone asked how such a program
worked in practice on a real computer,
it would have been interpreted as an in-
sult or perhaps simply as irrelevant.
eae The idea behind model check-
ing was to avoid having humans con-
struct proofs. It turns out that many
important programs, such as operating
systems, have ongoing behavior and
ideally run forever; they don’t just start
and stop. In 1977, Amir Pnueli suggest-
ed that temporal logic could be a good
way to describe and reason about these
programs. Now, if a program can be
specified in temporal logic, then it can
be realized as a finite state program—
a program with just a finite number
of different configurations. This sug-
gested the idea of model checking—to
check whether a finite state graph is a
model of a temporal logic specifica-
tion. Then one can develop efficient
algorithms to check whether the tem-
poral-logic specification is true of the
state graph by searching through the
state graph for certain patterns.
emc Yes, Allen and I noticed that
many concurrent programs had what
we called “finite state synchronization
skeletons.” (Joseph Sifakis and J.P.
Queille made the same observation, independently.) For example, the part of
a mutual-exclusion program that handles synchronization does not depend