Gerard J. Holzmann was born in 1951. He is a Dutch and American computer scientist and researcher at Bell Labs and NASA. He is most famous for creating the SPIN model checker.

Early life and education

Holzmann was born in Amsterdam, Netherlands. He earned an Engineer's degree in electrical engineering from Delft University of Technology in 1976. Later, he received his PhD degree from Delft University in 1979. His advisors were Willem van der Poel and J.L. de Kroes. His thesis was titled "Coordination problems in multiprocessing systems." After receiving a Fulbright Scholarship, he became a graduate student at the University of Southern California for one more year. During this time, he worked with Per Brinch Hansen.

Career

In 1980, he began working at Bell Labs in Murray Hill for one year. He then returned to the Netherlands and worked as an assistant professor at Delft University of Technology for two years. In 1983, he went back to Bell Labs, where he worked in the Computing Science Research Center, which was formerly known as the Unix research group. In 2003, he joined NASA, where he currently leads the NASA JPL Laboratory for Reliable Software in Pasadena, California, and holds the title of JPL fellow.

In 1981, Holzmann received the Prof. Bahler Prize from the Royal Dutch Institute of Engineers. In 2001, he was honored with the Software System Award (for SPIN) by the Association for Computing Machinery (ACM). In 2002, he was chosen to receive the ACM SIGSOFT Outstanding Research Award. In 2005, he was selected for the Paris Kanellakis Theory and Practice Award. In the same year, he was elected as a member of the US National Academy of Engineering for creating systems that check if software works correctly. In 2011, he was inducted as a Fellow of the Association for Computing Machinery. In October 2012, he was awarded the NASA Exceptional Engineering Achievement Medal. In 2015, he received the IEEE Harlan D. Mills Award.

Work

Holzmann created the SPIN model checker, which stands for Simple Promela Interpreter, in the 1980s at Bell Labs. This tool checks if concurrent software works correctly and has been free to use since 1991.

Books

Publications: A list includes:

• The Spin Model Checker — Primer and Reference Manual. Published by Addison-Wesley in 2003. ISBN 0-321-22862-6.
• Design and Validation of Computer Protocols. Published by Prentice Hall in 1991.
• The Early History of Data Networks. Published by IEEE Computer Society Press in 1995.
• Beyond Photography — The Digital Darkroom. Published by Prentice Hall in 1988. ISBN 0-13-074410-7.