Gerard Holzmann

A key problem in computer science is finding ways to verify that hardware and software designs meet their specifications. This problem is particularly acute in reactive systems, which are systems that interact with their environments, such as digital systems and communication protocols. The four awardees demonstrated that checking the correctness of reactive systems can be done based on a mathematical analysis of automata. Specifically, questions about correctness of reactive systems with respect to expressive specifications can be reduced to questions about finite automata on infinitary input structures. They showed how this approach enables the development of algorithms that could be made efficient enough to automate reasoning in practice. Carrying out the automata-theoretic approach required advances in both automata theory and the theory of program logics. This connection brought a wealth of new techniques to the theory of program logics, and the new application revived the theory of automata on infinitary inputs. Their body of work provided the algorithmic foundations for many formal-verification tools. Furthermore, they were personally involved in the development of industrial verification tools via technology transfer and the development of the verification systems COSPAN and SPIN. Their techniques are widely used commercially in the development of "control-intensive" software programs.