Gerard J. Holzmann

Developer of the SPIN model checker, Holzmann is a Dutch-born American computer scientist and researcher known for his work at Bell Labs in Murray Hill, New Jersey and at NASA. SPIN (short for Simple Promela Interpreter) is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion, developed in the 1980s, and has been freely available since 1991. He has also been listed as a Senior Faculty Associate in Computing and Mathematical Sciences at Caltech in Pasadena, California.

He was born in Amsterdam, Netherlands and received his B.S. degree in 1973 and his M.S. degree in 1976, both in Electrical Engineering, from the Delft University of Technology. Holzmann earned his Ph.D. degree, also from Delft University, in 1979 under W.L. van der Poel and J.L. de Kroes, with a thesis entitled Coordination problems in multiprocessing systems. After receiving a Fulbright Scholarship he attended the University of Southern California as a post-graduate student for another year, where he worked with Per Brinch Hansen.

In 1980 he joined Bell Labs for a year and then returned to the Netherlands to serve as Assistant Professor at the Delft University of Technology for two years. In 1983 Holzmann went back to Bell Labs, where he worked in the Computing Science Research Center (the former UNIX research group). In 2003 he joined NASA, where he led the NASA JPL Laboratory for Reliable Software in Pasadena, California and served as a JPL fellow.

In 1981 he was awarded the Prof. Bahler Prize by the Royal Dutch Institute of Engineers, the Paris Kanellakis Theory and Practice Award in 2005, and the NASA Exceptional Engineering Achievement Medal in October 2012. In 2015 Holzmann was named a recipient of the IEEE Computer Society Harlan D. Mills Award "for fundamental contributions to improving software quality, in particular through model-checking tools and coding standards, and for successfully transferring these contributions to practitioners developing mission-critical software." The Mills Award recognizes researchers and practitioners who have demonstrated longstanding contributions to information science theory and practice, focusing on applying sound theory to software engineering practice.

He is a member of the U.S. National Academy of Engineering, and in 2011 he was inducted as a Fellow of the Association for Computing Machinery. Among his numerous publications are: "The Spin Model Checker — Primer and Reference Manual", Addison-Wesley, 2003, ISBN 0-321-22862-6; "Design and Validation of Computer Protocols", Prentice Hall, 1991; "The Early History of Data Networks", IEEE Computer Society Press, 1995; and "Beyond Photography — The Digital Darkroom", Prentice Hall, 1988, ISBN 0-13-074410-7.