Greg Nelson (počítačový vědec) - Greg Nelson (computer scientist)

Greg Nelson
narozený
Charles Gregory Nelson

(1953-03-27)27. března 1953
Zemřel2. února 2015(2015-02-02) (ve věku 61)
Známý jakoteorie uspokojivosti modulo, rozšířená statická kontrola, ověření programu,
OceněníHerbrand Award (2010)

Charles Gregory Nelson (27. března 1953 - 2. února 2015) byl americký počítačový vědec.

Životopis

Nelson vyrostl v Honolulu. Jako chlapec vynikal v gymnastice a tenise. Navštěvoval univerzitní laboratorní školu. Získal titul B.A. titul z matematiky z Harvardská Univerzita v roce 1976. Získal titul Ph.D. v informatice od Stanfordská Univerzita v roce 1980 pod dohledem Robert Tarjan. Žil v Juneau po dobu jednoho roku, než se trvale usadí v Oblast zálivu San Francisco.

Pozoruhodná práce

Jeho diplomová práce ovlivnila obojí ověření programu a automatizované dokazování věty, zejména v oblasti nyní známé jako teorie uspokojivosti modulo, kde přispěl technikami kombinování rozhodovací postupy, stejně jako účinné rozhodovací postupy pro omezení bez kvantifikátoru v logika prvního řádu a termínová algebra. Obdržel Herbrand Award v roce 2013:

za jeho průkopnické příspěvky k dokazování teorémů a verifikaci programu, jako je jeho klíčová práce s Derekem Oppenem o kombinaci postupů uspokojivosti a algoritmů rychlého uzavření kongruence, vývoj vysoce vlivného testeru teorémů Simplify a jeho role při vytváření pole rozšířené statické kontroly.

Podílel se na vývoji ověřovače věty Simplify, který používal ESC / Java Významně přispěl také v několika dalších oblastech. Přispěl do oblasti programovacího jazyka jako člen Modula-3 výbor. V distribuovaných systémech přispíval do Network Objects. Průkopnicky přispěl svými omezujícími grafickými editory (Juno a Juno-2), okenními systémy (Trestle), optimálními generování kódu (Denali) a vícevláknové programování (Guma).

externí odkazy