Greg Nelson (datavetare)

Greg Nelson
Född	Charles Gregory Nelson ( 1953-03-27 ) 27 mars 1953
dog	2 februari 2015 (2015-02-02) (61 år)
Utbildning	BA, Harvard University (1976) Ph.D., Stanford University (1980)
Känd för	Tillfredsställelse modulo teorier Utökad statisk kontroll Programverifiering Modula-3 kommitté ESC/Java Förenkla satsprover
Utmärkelser	Herbrand Award (2013)
Vetenskaplig karriär
institutioner	Xerox Palo Alto Research Center (PARC) Digital Equipment Corporation (DEC) Systems Research Center (SRC) Hewlett-Packard Labs
Avhandling	Tekniker för programverifiering (1980)
Doktorand rådgivare	Robert Tarjan

Charles Gregory Nelson (27 mars 1953 – 2 februari 2015) var en amerikansk datavetare .

Biografi

Nelson växte upp i Honolulu . Som pojke utmärkte han sig i gymnastik och tennis. Han gick på University Laboratory School. Han tog sin BA-examen i matematik från Harvard University 1976. Han tog sin Ph.D. i datavetenskap från Stanford University 1980 under ledning av Robert Tarjan . Han bodde i Juneau, Alaska i ett år innan han bosatte sig permanent i San Francisco Bay Area .

Anmärkningsvärt arbete

Hans avhandling, Techniques for Program Verification , påverkade både programverifiering och automatiserad teorembevisande, särskilt inom det område som nu kallas satisfiability modulo theories, där han bidrog med tekniker för att kombinera beslutsprocedurer , såväl som effektiva beslutsprocedurer för kvantifieringsfria begränsningar i första- ordningslogik och termalgebra . Han fick Herbrand Award 2013:

för hans banbrytande bidrag till satsbevisande och programverifiering, såsom hans framstående arbete med Derek Oppen om kombinationen av tillfredsställelseprocedurer och snabba kongruensstängningsalgoritmer, utvecklingen av den mycket inflytelserika satsbevisaren Simplify och hans roll i skapandet av fältet utökad statisk kontroll.

Han var avgörande för att utveckla Simplify theorem prover som användes av ESC/Java . Han gjorde betydande insatser på flera andra områden. Han bidrog till området programmeringsspråkdesign som medlem i Modula-3- kommittén. I distribuerade system bidrog han till Network Objects. Han gjorde banbrytande bidrag med sina begränsningsbaserade grafikredigerare (Juno och Juno-2), fönstersystem (Trestle), optimal kodgenerering (Denali) och flertrådsprogrammering ( Eraser).

Se även

• Lista över datavetare
• Lista över programmerare