turing lecture
Doi: 10.1145/1592761.1592781
Turing Lecture from the winners of
the 2007 ACM A.M. Turing Award.
In 1981, Edmund M. Clarke and E. Allen Emerson, working in the
USA, and Joseph Sifakis working independently in France, authored
seminal papers that founded what has become the highly successful
field of model checking. This verification technology provides an
algorithmic means of determining whether an abstract model—
representing, for example, a hardware or software design—satisfies
a formal specification expressed as a temporal logic (TL) formula.
Moreover, if the property does not hold, the method identifies a
counterexample execution that shows the source of the problem.
The progression of model checking to the point where it can be
successfully used for complex systems has required the development
of sophisticated means of coping with what is known as the state
explosion problem. Great strides have been made on this problem
over the past 28 years by what is now a very large international
research community. As a result many major hardware and software
companies are beginning to use model checking in practice.
Examples of its use include the verification of VLSI circuits,
communication protocols, software device drivers, real-time
embedded systems, and security algorithms.
The work of Clarke, Emerson, and Sifakis continues to be central
to the success of this research area. Their work over the years has
led to the creation of new logics for specification, new verification
algorithms, and surprising theoretical results. Model checking tools,
created by both academic and industrial teams, have resulted in an
entirely novel approach to verification and test case generation. This
approach, for example, often enables engineers in the electronics
industry to design complex systems with considerable assurance
regarding the correctness of their initial designs. Model checking
promises to have an even greater impact on the hardware and
software industries in the future.
—Moshe Y. Vardi, Editor-in-Chief
