Information
Membership Number: FCA3513
Membership Type: Fellowship
Division: Engineering and Applied Sciences
Corresponding Email: gholzmann@acm.org
Homepage(s): https://spinroot.com/gerard/
Present and Previous Positions
Lecturer of Computer Science, Caltech CMS
Nimble Research, CA, research contracts
Fields of Scholarship and Research Interests
Software reliability/safety, static source code analysis, code review, formal verification, concurrency, distributed systems, logic model checking, software engineering, software tools, formal methods
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 concurrent software, since 1991 freely available.
Honors, Awards and Other Membership
Member of the U.S. National Academy of Engineering (2005)
JPL Fellow (2007)
ACM Fellow (2012)
AAIA Fellow (2022)
TS/SCI (2015-2017)
2022 Elected Fellow of the Asia-Pacific Artificial Intelligence Association (Aug. 2022)
2016 Named one of ten "Dutch Superheros in IT" by Intermediair (Nov. 2016)
2015 IEEE Har lan D. Mills Award
"For fundamental contributions to improving software quality, in particular through model checking tools and coding standards, and for successfully transferring these contributions to practitioners developing mission-critical software."
2013 NASA Software of the Year Award
Mars Science Laboratory (MSL), Flight Software Team (Nov. 2013)
2013 NASA Group Achievement Award, MSL Flight Software Team (Oct. 2013)
"For outstanding achievement in the design and development of the Mars Science Laboratory Flight Software."
2013 JPL Research Poster Conference Award Winner (Jan. 2013)
"Verification methods and structur ing pr inciples for reliable software development"
2012 NASA Exceptional Engineering Achievement Medal (Oct. 2012)
"for exceptional and sustained achievement in developing and infusing advanced engineering practices for the verification of mission-critical software"
2012 ACM Fellow (June 2012)
"for contributions to software verification by model checking"
2011 NASA Group Achievement Award
To the Unintended Acceleration Assessment Team (Oct. 2011)
"for outstanding technical expertise and dedicated support to the NASA Engineering and Safety Center’s investigation of unintended acceleration in Toyota vehicles"
2009 NASA Space Act Award (Aug. 2009)
"for the development of a significant scientific or technical contribution, entitled Support for systematic code reviews with the Scrub tool"
2007 JPL Fellow (Apr il 2007)
"In recognition of his outstanding leadership and technical contributions in the development of reliable software systems, in pioneering the application of logic model checking techniques to software verification, and in infusing these techniques in the development of increasingly complex space missions"
2006 Doctor Honoris Causa, Twente University, The Netherlands (Dec. 2006)
2006 ACM Kanellakis Theory and Practice Award (with Kurshan, Vardi, and Wolper, May 2006) "for the development of automata-theoretic techniques for reactive-systems verification, and the practical realization of powerful formal verification tools based on these techniques"
2005 Elected member US National Academy of Engineering (Oct. 2005)
"For the creation of model checking systems for software verification"
2003 Thomas Alva Edison Patent Award, R&D Council of NJ (Nov. 2003)
"for Methods and Apparatus for testing Event-Driven Software, US Patent 6,353,896"
2002 ACM SIGSOFT Outstanding Research Award (Orlando, May 2002)
2001 ACM Software Systems Award for the Spin model checker (Toronto, Apr il 2002) "for the Spin verification system, a highly successful and widely used model-checking software system based on formal methods from Computer Science. Spin has made advanced theoretical verification methods applicable to large and highly complex software systems".
2000 Best Paper Award, Bell Labs Technical Journal
1998 Best Paper Award, ICRE Conference
1995 Distinguished Member of Technical Staff Award, Bell Labs
1981 Prof. Ba "hler Prize for best Dutch Ph.D. thesis 1975-1980 in Telecomm., 1st recipient
1979 Fulbright-Hayes Scholarship
Selected Publications
https://scholar.google.com/citations?user=thNT9QYAAAAJ&hl=en
Other Information
gjh_cv.pdf