Handbook of Model Checking，经典技术手册。

With 32 technical articles and 76 authors, this handbook represents a full postgraduate
course in Model Checking. If a reader can verify that he or she has read
and studied every article, then Springer should certainly award that reader a Master’s
Degree inModel Checking! Departments in Computer Science everywhere will
certainly welcome access to this major resource.
Model Checking has become a major area of research and development both
for hardware and software verification owing to many factors. First, the improved
speed and capacity of computers in recent times have made all kinds of problem
solving both practical and efficient. Moreover, in the area of Model Checking the
methods of design of models have contributed to the best formulation of problems.
Then we have seen SAT solvers gain unexpected and truly remarkable efficiency
improvements—despite theoretical limitations. Additionally, the methodology of
Satisfiability Modulo Theories (SMT) has contributed to finding excellent ways to
pose and solve problems. Uses of temporal logic and data-flow-analysis techniques
have also made model checking more naturally efficient. All these contributions
have helped solve the ever-present “state explosion problem.” The urgency to make
greater strides has increased because new applications in such diverse areas as health
care, transportation, security, and robotics require work in the field to achieve greater
scale, expressivity, and automation.
I would definitely recommend new Ph.D. candidates look seriously into going
into research in this field, because success in Model Checking can directly lead to
future success in many other activities in Computer Science.
Finally, the recent tragic loss of Helmut Veith has been a dreadful blow to his
family, friends, colleagues, and students. Let’s take up the flag in his honor to help
promote and expand the field in which he was poised to become a recognized world
leader.
Carnegie Mellon University Dana S. Scott
Department of Mathematics, University of California, Berkeley