Gerard J. Holzmann (nacido en 1951) es un científico informático holandés-estadounidense e investigador de Bell Labs y la NASA , mejor conocido como el desarrollador del verificador de modelos SPIN . [1]
Holzmann nació en Ámsterdam , Países Bajos , y se licenció en ingeniería eléctrica en la Universidad Tecnológica de Delft en 1976. Posteriormente, en 1979, también obtuvo su doctorado en la Universidad de Delft bajo la dirección de Willem van der Poel y JL de Kroes, con una tesis titulada Problemas de coordinación en sistemas de multiprocesamiento . Tras recibir una beca Fulbright, realizó un año más de posgrado en la Universidad del Sur de California , donde trabajó con Per Brinch Hansen .
En 1980 empezó a trabajar en Bell Labs en Murray Hill durante un año. De regreso a los Países Bajos, fue profesor asistente en la Universidad Tecnológica de Delft durante dos años. [2] En 1983 regresó a Bell Labs , donde trabajó en el Centro de Investigación en Ciencias de la Computación (el antiguo grupo de investigación Unix ). En 2003 se unió a la NASA , donde dirige el Laboratorio de Software Fiable del JPL de la NASA [3] en Pasadena , California , y es miembro del JPL. [1]
En 1981, Holzmann recibió el Premio Prof. Bahler del Real Instituto Holandés de Ingenieros. [2] En 2001, fue seleccionado para el Premio de Sistema de Software (por SPIN) por la Asociación de Maquinaria Informática (ACM). En 2002, fue seleccionado para el Premio de Investigación Sobresaliente ACM SIGSOFT . [4] Fue seleccionado para el Premio de Teoría y Práctica Paris Kanellakis en 2005. [1] Fue elegido miembro de la Academia Nacional de Ingeniería de EE. UU. en 2005 por la creación de sistemas de verificación de modelos para la verificación de software. [5] En 2011 fue incluido como miembro de la Asociación de Maquinaria Informática . [6] Fue galardonado con la Medalla de Logro Excepcional de Ingeniería de la NASA en octubre de 2012. [1] En 2015 fue galardonado con el Premio IEEE Harlan D. Mills. [7]
Holzmann es conocido por desarrollar el verificador de modelos SPIN (SPIN es la abreviatura de Simple Promela Interpreter ) en los Laboratorios Bell en la década de 1980. Este dispositivo puede verificar la corrección del software concurrente y está disponible de forma gratuita desde 1991.
Publicaciones, una selección: [8]