Gerard J. Holzmann | |
---|---|
Born | 1951 |
Alma mater | Delft University of Technology |
Known for | Developing 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]
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] In 2001, he was selected for the Software System Award (for SPIN) by the Association for Computing Machinery (ACM). In 2002, he was selected for the ACM SIGSOFT Outstanding Research Award. [4] He was selected for the Paris Kanellakis Theory and Practice Award in 2005. [1] He was elected a member of the US National Academy of Engineering in 2005 for the creation of model-checking systems for software verification. [5] In 2011 he was inducted as a Fellow of the Association for Computing Machinery. [6] He was awarded the NASA Exceptional Engineering Achievement Medal in October 2012. [1] In 2015 he was awarded the IEEE Harlan D. Mills Award. [7]
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.
Publications, a selection: [8]
The Association for Computing Machinery (ACM) is a US-based international learned society for computing. It was founded in 1947 and is the world's largest scientific and educational computing society. The ACM is a non-profit professional membership group, reporting nearly 110,000 student and professional members as of 2022. Its headquarters are in New York City.
Software engineering is an engineering approach to software development. A practitioner, called a software engineer, applies the engineering design process to develop software.
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.
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.
Harlan D. Mills was professor of computer science at the Florida Institute of Technology and founder of Software Engineering Technology, Inc. of Vero Beach, Florida. Mills' contributions to software engineering have had a profound and enduring effect on education and industrial practice. Since earning his Ph.D. in Mathematics at Iowa State University in 1952, Mills led a distinguished career.
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.
Victor R. Basili, is an emeritus professor at the Department of Computer Science, which is part of the University of Maryland College of Computer, Mathematical, and Natural Sciences, and the Institute for Advanced Computer Studies. He holds a Ph.D. in computer science from the University of Texas at Austin and two honorary degrees. He is a fellow of both the Association for Computing Machinery (ACM) and of the Institute of Electrical and Electronics Engineers (IEEE).
Carlo Ghezzi is an emeritus professor and former chair of software engineering at the Politecnico di Milano, Italy, and an adjunct professor at the Università della Svizzera italiana (USI), Switzerland. At the Politecnico, he has been the Rector's Delegate for research, department chair, head of the PhD program, and member of the academic senate and of the board of governors of Politecnico.
Mary Lou Ehnot Soffa is an American computer scientist noted for her research on compilers, program optimization, system software and system engineering.
Lori A. Clarke is an American computer scientist noted for her research on software engineering.
Leon Joel Osterweil is an American computer scientist noted for his research on software engineering.
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.
T.H. Tse is a Hong Kong academic who is a professor and researcher in program testing and debugging. He is ranked internationally as the second most prolific author in metamorphic testing. According to Bruel et al., "Research on integrated formal and informal techniques can trace its roots to the work of T.H. Tse in the mid-eighties." The application areas of his research include object-oriented software, services computing, pervasive computing, concurrent systems, imaging software, and numerical programs. In addition, he creates graphic designs for non-government organizations.
Axel van Lamsweerde is a Belgian computer scientist and Professor of Computing Science at the Universite catholique de Louvain, known for his work on requirements engineering and the development of the KAOS goal-oriented modeling language.
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 2001, and was the 2017 recipient of the Harlan D. Mills Award from the IEEE Computer Society.
Tore Dybå is a Norwegian scientist and software engineer in the fields of information systems and computer science. He has been a Chief Scientist at SINTEF ICT since 2003.
Marvin Victor Zelkowitz is an American computer scientist and engineer.
Corina S. Păsăreanu is a Romanian-American computer scientist with affiliations at the NASA Ames Research Center, with the Carnegie Mellon University CyLab Security and Privacy Institute, and with KBR. Her research involves formal methods, including symbolic execution and the verification of systems of interacting components. She is the author of the book Symbolic Execution and Quantitative Reasoning: Applications to Software Safety and Security.