Gerard J. Holzmann

Last updated
Gerard J. Holzmann
Gerard J. Holzmann FLoC 2006.jpg
Gerard J. Holzmann 2006
Born1951 (1951)
Alma mater Delft University of Technology
Known forDeveloping the SPIN model checker
Awards Paris Kanellakis Award (2005)
Scientific career
Fields Model Checking
Institutions Bell Labs
Doctoral advisor Willem van der Poel and J.L. de Kroes

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

Contents

Biography

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 Willem 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.

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 joined 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 Software System Award (for SPIN) in 2001 by the Association for Computing Machinery (ACM), the Paris Kanellakis Theory and Practice Award in 2005, and the NASA Exceptional Engineering Achievement Medal in October 2012. [1] Holzmann was elected a member of the US National Academy of Engineering in 2005 for the creation of model-checking systems for software verification. [4] In 2011 he was inducted as a Fellow of the Association for Computing Machinery. [5] In 2015 he was awarded the IEEE Harlan D. Mills Award. [6]

Work

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.

Books

Publications, a selection: [7]

Related Research Articles

<span class="mw-page-title-main">Alfred Aho</span> Canadian computer scientist

Alfred Vaino Aho is a Canadian computer scientist best known for his work on programming languages, compilers, and related algorithms, and his textbooks on the art and science of computer programming.

<span class="mw-page-title-main">Model checking</span> Computer science field

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

<span class="mw-page-title-main">Bob Kahn</span> American Internet pioneer, computer scientist

Robert Elliot Kahn is an American electrical engineer who, along with Vint Cerf, first proposed the Transmission Control Protocol (TCP) and the Internet Protocol (IP), the fundamental communication protocols at the heart of the Internet.

<span class="mw-page-title-main">Peter G. Neumann</span> American computer scientist

Peter Gabriel Neumann is a computer-science researcher who worked on the Multics operating system in the 1960s. He edits the RISKS Digest columns for ACM Software Engineering Notes and Communications of the ACM. He founded ACM SIGSOFT and is a Fellow of the ACM, IEEE, and AAAS.

<span class="mw-page-title-main">Stuart Feldman</span> American computer scientist

Stuart Feldman is an American computer scientist. He is best known as the creator of the computer software program make. He was also an author of the first Fortran 77 compiler, was part of the original group at Bell Labs that created the Unix operating system, and participated in development of the ALTRAN and EFL programming languages.

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 at Bell Labs, beginning in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field.

Scott J. Shenker is an American computer scientist, and professor of computer science at the University of California, Berkeley. He is also the leader of the Extensible Internet Group at the International Computer Science Institute in Berkeley, California.

Kanianthra Mani Chandy is the Simon Ramo Professor of Computer Science at the California Institute of Technology (Caltech). He has been the Executive Officer of the Computer Science Department twice, and he has been a professor at Caltech since 1989. He also served as Chair of the Division of Engineering and Applied Science at the California Institute of Technology.

<span class="mw-page-title-main">Gernot Heiser</span> Australian computer scientist

Gernot Heiser is a Scientia Professor and the John Lions Chair for operating systems at UNSW Sydney, where he leads the Trustworthy Systems group (TS).

Arvind is the Johnson Professor of Computer Science and Engineering in the Computer Science and Artificial Intelligence Laboratory (CSAIL) at the Massachusetts Institute of Technology (MIT). He is a Fellow of the Institute of Electrical and Electronics Engineers (IEEE) and the Association for Computing Machinery (ACM). He was also elected as a member into the National Academy of Engineering in 2008 for contributions to dataflow and multithread computing and the development of tools for the high-level synthesis of digital electronics hardware.

Krishan Sabnani is an Indian-American networking researcher. He has made many seminal contributions to the Internet infrastructure design, protocol design, and wireless networks. Krishan made a breakthrough in Internet re-design. The main idea behind this work was to separate control functions and complex software from the forwarding portions on Internet routers. This work made it possible for forwarding technologies to evolve and be deployed independently from control protocols. This contribution is a precursor to the current Software Defined Networking (SDN) revolution. A patent based on this work won the 2010 Edison Patent Award.

Elaine Jessica Weyuker is an ACM Fellow, an IEEE Fellow, and an AT&T Fellow at Bell Labs for research in software metrics and testing as well as elected to the National Academy of Engineering. She is the author of over 130 papers in journals and refereed conference proceedings.

<span class="mw-page-title-main">Sundaraja Sitharama Iyengar</span> Indian computer scientist (born 1947)

Sundaraja Sitharama Iyengar is an Indian-born American computer scientist and the Distinguished University Professor, Ryder Professor and Director of Computer Science at Florida International University, Miami, Florida, USA. He also founded and directs the Robotics Research Laboratory at Louisiana State University (LSU). He has been a visiting professor or scientist at Oak Ridge National Laboratory, Jet Propulsion Laboratory, Naval Research Laboratory, and has been awarded the Satish Dhawan Visiting Chaired Professorship at the Indian Institute of Science, the Homi Bhaba Visiting Chaired Professor (IGCAR), and a professorship at the University of Paris (Sorbonne).

<span class="mw-page-title-main">Marta Kwiatkowska</span> British computer scientist

Marta Zofia Kwiatkowska is a Polish theoretical computer scientist based in the United Kingdom.

Ravishankar K. Iyer is the George and Ann Fisher Distinguished Professor of Engineering at the University of Illinois at Urbana-Champaign. He is a specialist in reliable and secure networks and systems.

Kenneth P. Birman is a professor in the Department of Computer Science at Cornell University. He currently holds the N. Rama Rao Chair in Computer Science.

Alexander L. Wolf is an American computer scientist known for his research in software engineering, distributed systems, and computer networking. He is credited, along with his collaborators, with introducing the modern study of software architecture, content-based publish/subscribe messaging, content-based networking, automated process discovery, and the software deployment lifecycle. Wolf's 1985 Ph.D. dissertation developed language features for expressing a module's import/export specifications and the notion of multiple interfaces for a type, both of which are now common in modern computer programming languages.

Pamela Zave is an American computer scientist now working at Princeton University. She is known for her work on requirements engineering, telecommunication services, and protocol modeling and verification, and is now working on network architecture. She was named a Fellow of the Association for Computing Machinery in 2002, and was the 2017 recipient of the Harlan D. Mills Award from the IEEE Computer Society.

Norman Paul Jouppi is an American electrical engineer and computer scientist.

Marvin Victor Zelkowitz is an American computer scientist and engineer.

References

  1. 1 2 3 "spin" . Retrieved 8 January 2011.
  2. 1 2 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". Archived from the original on 2019-01-19. Retrieved 2019-12-27.
  4. NAE Members
  5. Gerard J. Holzmann, ACM Fellows United States – 2011 at awards.acm.org.
  6. "2014 Mills Award to Holzmann | IEEE Computer Society". 13 April 2018.
  7. DBLP bibliography