Gerard J. Holzmann (* 1951 in Amsterdam) ist ein niederländischer Informatiker.
Holzmann studierte an der TU Delft Informatik mit dem Diplom 1976 und wurde dort 1979 bei W. L. van der Poel und J. L. de Kroes promoviert (Coordination problems in multiprocessing systems). Als Post-Doktorand war er bei Per Brinch Hansen in Los Angeles als Fulbright-Stipendiat und 1980/81 bei den Bell Laboratories angestellt. Dort blieb er (bis auf eine Zeit als Assistenzprofessor in Delft 1981 bis 1983) bis 2003. Er war ab 1995 Distinguished Member of Technical Staff bei Bell Labs und ab 2001 Direktor Computer Principles Research. Ab 2003 war er leitender Informatiker am Jet Propulsion Laboratory (JPL) der NASA und leitender Wissenschaftler im Labor für Software-Zuverlässigkeit. Außerdem war er in der Informatik Fakultät des Caltech.
In den 1980er Jahren entwickelte er an den Bell Labs den SPIN Model Checker zur Verifikation der Korrektheit verteilter Software. SPIN steht für Simple Promela Interpreter, wobei Promela (Process oder Protocol Meta Language) für eine Beschreibungssprache steht. Seit 1991 ist SPIN frei verfügbar.
2012 erhielt er einen Exceptional Engineering Achievement Award der NASA und 2009 den Space Act Award der NASA. 2012 wurde er ACM Fellow und 2007 Fellow des JPL und 2005 Fellow der National Academy of Engineering. 2006 wurde er Ehrendoktor der Universität Twente. 2005 erhielt er mit anderen den Paris-Kanellakis-Preis und 2001 den ACM Software System Award.
Schriften
- 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 (das Buch prägte den Begriff Digital Darkroom für Fotobearbeitung mit Computern)