Dr. Gerard J. Holzmann

A Dutch-born American computer scientist and researcher at Bell Labs in Murray Hill, New Jersey and at NASA, he is best known as the developer in the 1980s of the SPIN model checker - a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. SPIN, (short for Simple Promela Interpreter) has been freely available since 1991. He is also 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. He 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 was a post-graduate student at the University of Southern California 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 he 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 leads the NASA JPL Laboratory for Reliable Software in Pasadena, California and is 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 he 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.