Gerard J. Holzmann

From Wikipedia, the free encyclopedia
Jump to: navigation, search
Gerard J. Holzmann
Gerard J. Holzmann FLoC 2006.jpg
Gerard J. Holzmann 2006
Born 1951 (1951)
Amsterdam, Netherlands
Nationality American
Fields Model Checking
Institutions Bell Labs
Alma mater Delft University of Technology
Doctoral advisor Willem van der Poel and J.L. de Kroes
Known for Developing the SPIN model checker
Notable awards Paris Kanellakis Award (2005)

Gerard J. Holzmann (born 1951) is an Dutch-born American computer scientist and researcher at Bell Labs and NASA, best known as the developer of the SPIN model checker.[1]

Biography[edit]

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 W.L. van der Poel and J.L. de Kroes with a thesis entitled Coordination problems in multiprocessing systems. After receiving a Fulbright Scholar he was post-graduate student at the University of Southern California for another year, where he worked with Per Brinch Hansen.

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.[2] In 1983 he returned to Bell Labs where he worked in the Computing Science Research Center (the former Unix research group). In 2003 he jointed NASA, where he leads the NASA JPL Laboratory for Reliable Software[3] in Pasadena, California and is a JPL fellow.[1]

In 1981 Holzmann was awarded the Prof. Bahler Prize by the Royal Dutch Institute of Engineers,[2] the Paris Kanellakis Theory and Practice Award in 2005, and the NASA Exceptional Engineering Achievement Medal in October 2012.[1] Holzmann is a member of the US National Academy of Engineering. In 2011 he was inducted as a Fellow of the Association for Computing Machinery.[4]

Work[edit]

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 distributed software, since 1991 freely available.

Books[edit]

Publications, a selection:[5]

References[edit]

  1. ^ a b c "spin". Retrieved 8 January 2011. 
  2. ^ a b Holzmann, Gerard J. "The Pandora System: an interactive system for the design of data communication protocols." Computer Networks (1976) 8.2 (1984): 71-79.
  3. ^ Laboratory for Reliable Software
  4. ^ Gerard J. Holzmann, ACM Fellows United States – 2011 at awards.acm.org.
  5. ^ DBLP bibliography

External links[edit]