Gerard J. Holzmann (born 1951) is a Dutch-American
computer scientist and researcher at
Bell Labs
Nokia Bell Labs, originally named Bell Telephone Laboratories (1925–1984),
then AT&T Bell Laboratories (1984–1996)
and Bell Labs Innovations (1996–2007),
is an American industrial Research and development, research and scientific developm ...
and
NASA
The National Aeronautics and Space Administration (NASA ) is an independent agencies of the United States government, independent agency of the US federal government responsible for the civil List of government space agencies, space program ...
, best known as the developer of the
SPIN model checker
SPIN is a general tool for verifying the correctness of concurrent software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center ...
.
Biography
Holzmann was born in
Amsterdam
Amsterdam ( , , , lit. ''The Dam on the River Amstel'') is the capital and most populous city of the Netherlands, with The Hague being the seat of government. It has a population of 907,976 within the city proper, 1,558,755 in the urban ar ...
,
Netherlands
)
, anthem = ( en, "William of Nassau")
, image_map =
, map_caption =
, subdivision_type = Sovereign state
, subdivision_name = Kingdom of the Netherlands
, established_title = Before independence
, established_date = Spanish Netherl ...
and received an
Engineer's degree in
electrical engineering from the
Delft University of Technology
Delft University of Technology ( nl, Technische Universiteit Delft), also known as TU Delft, is the oldest and largest Dutch public technical university, located in Delft, Netherlands. As of 2022 it is ranked by QS World University Rankings among ...
in 1976. He subsequently also received his
PhD degree from
Delft University
Delft University of Technology ( nl, Technische Universiteit Delft), also known as TU Delft, is the oldest and largest Dutch public technical university, located in Delft, Netherlands. As of 2022 it is ranked by QS World University Rankings among ...
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 Scholarship he was a post-graduate student at the University of Southern California for another year, where he worked with
Per Brinch Hansen
Per Brinch Hansen (13 November 1938 – 31 July 2007) was a Danish-American computer scientist known for his work in operating systems, concurrent programming and parallel and distributed computing.
Biography
Early life and education
Per B ...
.
In 1980 he started at
Bell Labs
Nokia Bell Labs, originally named Bell Telephone Laboratories (1925–1984),
then AT&T Bell Laboratories (1984–1996)
and Bell Labs Innovations (1996–2007),
is an American industrial Research and development, research and scientific developm ...
in Murray Hill for a year. Back in the Netherlands he was assistant professor at the Delft University of Technology for two years.
[Holzmann, Gerard J. "The Pandora System: an interactive system for the design of data communication protocols." ''Computer Networks'' (1976) 8.2 (1984): 71-79.] In 1983 he returned to
Bell Labs
Nokia Bell Labs, originally named Bell Telephone Laboratories (1925–1984),
then AT&T Bell Laboratories (1984–1996)
and Bell Labs Innovations (1996–2007),
is an American industrial Research and development, research and scientific developm ...
where he worked in the Computing Science Research Center (the former
Unix
Unix (; trademarked as UNIX) is a family of multitasking, multiuser computer operating systems that derive from the original AT&T Unix, whose development started in 1969 at the Bell Labs research center by Ken Thompson, Dennis Ritchie, an ...
research group). In 2003 he joined
NASA
The National Aeronautics and Space Administration (NASA ) is an independent agencies of the United States government, independent agency of the US federal government responsible for the civil List of government space agencies, space program ...
, where he leads the NASA
JPL ''Laboratory for Reliable Software'' in
Pasadena
Pasadena ( ) is a city in Los Angeles County, California, northeast of downtown Los Angeles. It is the most populous city and the primary cultural center of the San Gabriel Valley. Old Pasadena is the city's original commercial district.
...
,
California
California is a state in the Western United States, located along the Pacific Coast. With nearly 39.2million residents across a total area of approximately , it is the most populous U.S. state and the 3rd largest by area. It is also the m ...
and is a JPL fellow.
In 1981 Holzmann was awarded the Prof. Bahler Prize by the
Royal Dutch Institute of Engineers,
the
Software System Award
The ACM Software System Award is an annual award that honors people or an organization "for developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both". It is awarded by ...
(for Spin) in 2001 by the Association for Computing Machinery (ACM), the
Paris Kanellakis Theory and Practice Award The Paris Kanellakis Theory and Practice Award is granted yearly by the Association for Computing Machinery (ACM) to honor "specific theoretical accomplishments that have had a significant and demonstrable effect on the practice of computing". It wa ...
in 2005, and the
NASA Exceptional Engineering Achievement Medal
The NASA Exceptional Engineering Achievement Medal (abbreviated EEAM) was established by NASA in 1981 to recognize unusually significant engineering contributions towards achievement of aeronautical or space exploration goals. This award is given ...
in October 2012.
Holzmann was elected a member of the US
National Academy of Engineering
The National Academy of Engineering (NAE) is an American nonprofit, non-governmental organization. The National Academy of Engineering is part of the National Academies of Sciences, Engineering, and Medicine, along with the National Academy of ...
in 2005 for the creation of model-checking systems for software verification. In 2011 he was inducted as a Fellow of the
Association for Computing Machinery. In 2015 he was awarded th
IEEE Harlan D. Mills Award
Work
Holzmann is known for the development of the
SPIN model checker
SPIN is a general tool for verifying the correctness of concurrent software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center ...
(SPIN is short for ''Simple
Promela
PROMELA (Process or Protocol Meta Language) is a verification modeling language introduced by Gerard J. Holzmann. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, c ...
Interpreter'') in the 1980s at Bell Labs. This device can verify the correctness of
concurrent software, since 1991 freely available.
Books
Publications, a selection:
DBLP bibliography
/ref>
*
The Spin Model Checker — Primer and Reference Manual
', Addison-Wesley
Addison-Wesley is an American publisher of textbooks and computer literature. It is an imprint of Pearson PLC, a global publishing and education company. In addition to publishing books, Addison-Wesley also distributes its technical titles throu ...
, 2003. .
*
Design and Validation of Computer Protocols
', Prentice Hall, 1991.
*
The Early History of Data Networks
', IEEE
The Institute of Electrical and Electronics Engineers (IEEE) is a 501(c)(3) professional association for electronic engineering and electrical engineering (and associated disciplines) with its corporate office in New York City and its operat ...
Computer Society
The Institute of Electrical and Electronics Engineers (IEEE) is a 501(c)(3) professional association for electronic engineering and electrical engineering (and associated disciplines) with its corporate office in New York City and its operation ...
Press, 1995.
*
Beyond Photography — The Digital Darkroom
', Prentice Hall, 1988. .
References
External links
Home page
Interview
{{DEFAULTSORT:Holzmann, Gerard J
1951 births
Living people
American computer scientists
Dutch computer scientists
Formal methods people
Scientists at Bell Labs
Delft University of Technology alumni
Scientists from Amsterdam
NASA people
Dutch emigrants to the United States
Fellows of the Association for Computing Machinery
Members of the United States National Academy of Engineering
Fellows of Jet Propulsion Laboratory