Gerard J. Holzmann

Gerard J. Holzmann ( born 1951 in Amsterdam) is a Dutch computer scientist.

Holzmann studied at the TU Delft computer science with a diploma in 1976 and was there in 1979 his doctorate under WL van der Poel and JL de Kroes ( Coordination problems in multiprocessing systems). As a post - graduate student, he was employed by Per Brinch Hansen in Los Angeles as a Fulbright scholar and 1980/81 at Bell Laboratories. There he stayed ( except for a time as an assistant professor in Delft 1981 to 1983 ) until 2003. He was from 1995 Distinguished Member of Technical Staff at Bell Labs and since 2001 director of Computer Research Principles. From 2003 he was a senior computer scientist at the Jet Propulsion Laboratory ( JPL) of NASA and senior scientist in the laboratory for software reliability. He also appeared in the computer science faculty at Caltech.

In the 1980s he developed at Bell Labs the SPIN model checker to verify the correctness of distributed software. SPIN stands for Simple Promela Interpreter, with Promela (Process or Protocol Meta Language ) is a specification language. Since 1991, SPIN is freely available.

In 2012, he received an Exceptional Engineering Achievement Award from the NASA Space Act Award and 2009 NASA. In 2012 he became a Fellow of the ACM Fellow and 2007 JPL and 2005 Fellow of the National Academy of Engineering. In 2006 he became an honorary doctorate from the University of Twente. In 2005 he was awarded with the other Paris Kanellakis Award and the 2001 ACM Software System Award.

Writings

• 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 ( the book coined the term digital darkroom for photo editing with computers )