Gerard J. Holzmann

Holzmann was born in Amsterdam, Netherlands and received an Engineer's degree in electrical engineering from the Delft University of Technology in 1976. He subsequently also received his PhD degree from Delft University in 1979 under Willem 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. ==Career==

In 1980 he started at Bell Labs in Murray Hill for a year. Back in the Netherlands he was assistant professor at the Delft University of Technology for two years. In 1983 he returned 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. He was selected for the Paris Kanellakis Theory and Practice Award in 2005. In 2011 he was inducted as a Fellow of the Association for Computing Machinery. He was awarded the NASA Exceptional Engineering Achievement Medal in October 2012. == Work ==

Holzmann is known for the development of the SPIN model checker (SPIN is short for Simple Promela Interpreter) in the 1980s at Bell Labs. This device can verify the correctness of concurrent software, and has been freely available since 1991. == Books ==

Publications, a selection: • The Spin Model Checker — Primer and Reference Manual, Addison-Wesley, 2003. . • Design and Validation of Computer Protocols, Prentice Hall, 1991. • The Early History of Data Networks, IEEE Computer Society Press, 1995. • Beyond Photography — The Digital Darkroom, Prentice Hall, 1988. . ==See also==