Skip to main content
These web pages use cascading style sheet features for formatting. You may still browse the text of the site, but for best results, use a modern CSS-enabled browser.

Laboratory for Reliable Software (LaRS)
at the Jet Propulsion Laboratory

Title Image

Gerard Holzmann

Gerard's Picture
Address:
Jet Propulsion Laboratory
M/S 301-230A
4800 Oak Grove Drive
Pasadena, CA 91109
Phone:
818.393.5937
Fax:
818.393.0028
Email:
gh at jpl dot nasa dot gov
Homepage:
http://spinroot.com/gerard

Education

    • MSc (Ir.) Electrical Engineering, Delft University, The Netherlands (1976)
    • PhD Technical Sciences, Delft University, The Netherlands (1979)

Professional Experience

    • Senior Research Scientist (2005) and Fellow (2007), Systems and Software Division, Jet Propulsion Laboratory
    • Faculty Associate in Computer Science, Caltech, Pasadena (2007)
    • Director Computing Principles Research (2002-2003), Computing Science Research Center, Bell Laboratories, Murray Hill, NJ
    • Distinguished Member of Technical Staff (1995-2002), Computing Science Research Center, Bell Laboratories, Murray Hill, NJ
    • Member of Technical Staff (1980-2002), Computing Science Research Center, Bell Laboratories, Murray Hill, NJ
    • Researcher (1981-1983), Delft University, The Netherlands
    • Member of Technical Staff (1980-1981), Computing Science Research Center, Bell Laboratories, Murray Hill, NJ
    • Visiting Fullbright scholar (1979-1980), Computer Science, USC, Los Angeles, CA

Selected Awards

    • US National Academy of Engineering (elected 2005)
    • Doctor Honoris Causa, Twente University, The Netherlands (2006)
    • ACM Kanellakis Theory and Practice Award (co-recipient 2006)
    • Thomas Alva Edison Patent Award, R&D Council of NJ (2003)
    • ACM SIGSOFT Outstanding Research Award (2002)
    • ACM Software Systems Award (2002)
    • Prof Bahler Prize for best Dutch PhD thesis in telecomm 1975-1980 (1981)

Books

    • The Spin Model Checker: primer and reference manual, Addison-Wesley, 2004
    • The Early History of Data Networks, Wiley, 1995 (co-author Bjorn Pehrson)
    • Design and Validation of Computer Protocols, Prentice-Hall, 1991
    • Beyond Photograph, the digital darkroom, Prentice-Hall, 1988

Selected Recent Publications

    • G.J. Holzmann, R. Joshi, A. Groce, Model driven code checking, Automated Software Engineering Journal, Vol. 15, Nr. 3-4, pp. 283-297, Dec. 2008.
    • G.J. Holzmann, R. Joshi, A. Groce, Swarm Ver ification, Proc. ASE 2008, 23rd IEEE/ACM Int. Conf. on Automated Software Engineering, l'Aquila, Italy, Sept. 2008.
    • G.J. Holzmann and D. Bosnacki, The design of a multicore extension of the Spin model checker, IEEE Trans. on Software Engineering, Vol. 33, No. 10, pp. 659-674, Oct. 2007.
    • G.J.Holzmann and M.H. Smith, An automated ver ification method for distributed systems software based on model extraction, IEEE Trans. on Software Engineering, Vol. 28, No. 4, pp. 364-377, April 2002.
    • + More