Gerard J. Holzmann
| Gerard J. Holzmann | |
|---|---|
 | |
| Narození | 12. listopadu 1951 (72 let) Amsterdam |
| Bydliště | Amsterdam |
| Alma mater | Delftská technická univerzita (do 1979) |
| Povolání | informatik a inženýr |
| Zaměstnavatelé | Bellovy laboratoře (1980–2003) Jet Propulsion Laboratory (od 2003) |
| Ocenění | ACM Software System Award (2001) Paris Kanellakis Award (2005) ACM Fellow (2011) Harlan D. Mills Award (2015) |
| Některá data mohou pocházet z datové položky. | |
Gerard J. Holzmann (narozený v roce 1951 v Nizozemí) je americký informatik a vědec pracující v Bell Labs a NASA. Holzmann je známý tím, že stál u vzniku model checkeru SPIN.[1]
Život[editovat | editovat zdroj]
Holzmann se narodil v Amsterdamu v Nizozemí a získal v roce 1976 titul inženýr na fakultě elektrotechniky na TU Delft. Na stejné univerzitě získal v roce 1979 také Ph.D., jeho školitelem byl W.L. van der Poel a J.L. de Kroes, tématem jeho dizertační práce byla koordinace problémů v systémech s více procesy (Coordination problems in multiprocessing systems). Později Holzmann získal Fulbrightovo stipendium a působil rok na Univerzitě Jižní Kalifornie kde pracoval s Per Brinch Hansenem.
V roce 1980 začal pracovat v Bell Labs, kde zůstal jeden rok. Dále byl dva roky v Nizozemí odborným asistentem na TU Delft[2]. V roce 1983 se vrátil do Bell Labs kde pracoval v informatickém výzkumném centru. V roce 2003 začal pracovat v NASA, kde vede Laboratoř pro spolehlivý software[3] v Pasadeně v Kalifornii spadající pod NASA JPL.[1]
V roce 1981 získal cenu prof. Bahlera od Koninklijk Instituut van Ingenieurs,[2] v roce 2005 získal Paris Kanellakis Theory and Practice Award a v říjnu 2012 získal NASA Exceptional Engineering Achievement Medal.[1] Holzmann byl v roce 2005 zvolen do National Academy of Engineering v USA.[4] V roce 2011 se stal členem Association for Computing Machinery.[5]
Práce[editovat | editovat zdroj]
Holzmann je nejlépe známý jako autor model checkeru SPIN který začal tvořit v osmdesátých letech v Bell Labs. Tento nástroj dokáže formálně verifikovat korektnost distribuovaného software. SPIN je volně dostupný od roku 1991.
Publikace[editovat | editovat zdroj]
Výběr publikací:[6]
- 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.
- Beyond Photography — The Digital Darkroom, Prentice Hall, 1988. ISBN 0-13-074410-7.
Reference[editovat | editovat zdroj]
V tomto článku byl použit překlad textu z článku Gerard J. Holzmann na anglické Wikipedii.
- ↑ a b c spin [online]. [cit. 2011-01-08]. Dostupné online.
- ↑ a b Holzmann, Gerard J. "The Pandora System: an interactive system for the design of data communication protocols." Computer Networks (1976) 8.2 (1984): 71-79.
- ↑ Laboratory for Reliable Software. lars-lab.jpl.nasa.gov [online]. [cit. 2019-06-20]. Dostupné v archivu pořízeném dne 2019-01-19.
- ↑ NAE Members
- ↑ Gerard J. Holzmann, ACM Fellows United States – 2011 at awards.acm.org.
- ↑ DBLP bibliography. www.informatik.uni-trier.de [online]. [cit. 2016-02-27]. Dostupné v archivu pořízeném z originálu dne 2012-10-03.
