Gerard J. Holzmann

Gerard J. Holzmann

Gerard J. Holzmann (born 1951) is an American computer scientist, best known as the developer of the SPIN model checker.

Currently, Holzmann leads the NASA JPL "Laboratory for Reliable Software" in Pasadena, California. Previously he was at Bell Labs (c1980–2003) where he worked in the Computing Science Research Center (the former Unix research group).He was born in Amsterdam, The Netherlands and received an Engineer's degree in Electrical Engineering from the Delft University of Technology. He subsequently also received his PhD degree from Delft University in 1979. He is a member of the US National Academy of Engineering.

Books

* "The Spin Model Checker – Primer and Reference Manual", Addison-Wesley, 2003. ISBN 0-321-22862-6.
* "Design and Validation of Computer Protocols", Prentice Hall, 1991.
* "The Early History of Data Networks", IEEE Computer Society Press, 1995.
* " [http://www.spinroot.com/pico/ Beyond Photography – The Digital Darkroom] ", Prentice Hall, 1988. ISBN 0-13-074410-7

External links

* [http://spinroot.com/gerard/ Home page]
* [http://spinroot.com/whatispin.html Spin Tool]
* [http://spinroot.com/pico Pico image editor]
* [http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/h/Holzmann:Gerard_J=.html DBLP bibliography]
* [http://eis.jpl.nasa.gov/lars/ Laboratory for Reliable Software]
* [http://spinroot.com/gerard/portraits/index.html Portraits]


Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать курсовую

Look at other dictionaries:

  • SPIN — (ursprünglich ein Akronym für Simple PROMELA Interpreter) ist eines der bekanntesten Werkzeuge zur Modellprüfung (engl. Model Checking). SPIN prüft endliche Zustandsautomaten (engl. Finite State Machines) mit der temporalen Logik LTL. Zusätzlich… …   Deutsch Wikipedia

  • SPIN model checker — SPIN is a general tool for verifying the correctness of distributed software (software design) in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others, and has evolved for more than 15 years. SPIN is an… …   Wikipedia

  • Communications protocol — For other senses of this word, see Protocol. A communications protocol is a system of digital message formats and rules for exchanging those messages in or between computing systems and in telecommunications. A protocol may have a formal… …   Wikipedia

  • Model checking — This article is about checking of models in computer science. For the checking of models in statistics, see regression model validation. In computer science, model checking refers to the following problem: Given a model of a system, test… …   Wikipedia

  • Internetwork protocol — In networking, a communications protocol or network protocol is the specification of a set of rules for a particular type of communication.Multiple protocols often describe different aspects of a single communication. A group of protocols… …   Wikipedia

  • Partial order reduction — In computer science, partial order reduction is a technique for reducing the size of the state space to be searched by a model checking algorithm. It exploits the commutativity of concurrently executed transitions, which result in the same state… …   Wikipedia

  • Category:NASA personnel — v · d · …   Wikipedia

  • Équipe cycliste T-Mobile — T Mobile …   Wikipédia en Français

  • Semaphore line — This article is about the communication system using towers with pivoting shutters. For other uses, see Semaphore (disambiguation). For the now closed railway in Adelaide, Australia, see Semaphore railway line, Adelaide. A Chappe telegraph at… …   Wikipedia

  • Latin American music — Introduction       musical traditions of Mexico, Central America, and the portions of South America and the Caribbean colonized by the Spanish and the Portuguese. These traditions reflect the distinctive mixtures of Native American, African, and… …   Universalium

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”