Greg Nelson (computer scientist)
Greg Nelson | |
|---|---|
| Born | Charles Gregory Nelson March 27, 1953 |
| Died | February 2, 2015 (aged 61) |
| Known for | satisfiability modulo theories, extended static checking, program verification, |
| Awards | Herbrand Award (2010) |
Charles Gregory "Greg" Nelson (27 March 1953 – 2 February 2015) was an American computer scientist.
Biography
Nelson grew up in Honolulu. As a boy he excelled at gymnastics and tennis. He attended the University Laboratory School. He received his B.A. degree in mathematics from Harvard University in 1976. He received his Ph.D. in computer science from Stanford University in 1980 under the supervision of Robert Tarjan. He lived in Juneau for a year before settling permanently in the San Francisco Bay Area.
Notable work
His thesis work influenced both program verification and automated theorem proving, especially in the area now known as satisfiability modulo theories, where he contributed techniques for combining decision procedures, as well as efficient decision procedures for quantifier-free constraints in first-order logic and term algebra. He received the Herbrand Award in 2013:
for his pioneering contributions to theorem proving and program verification, such as his seminal work with Derek Oppen on the combination of satisfiability procedures and fast congruence closure algorithms, the development of the highly influential theorem prover Simplify, and his role in the creation of the field of extended static checking.
He was instrumental in the development of the Simplify theorem prover used by ESC/Java. He also made significant contributions in several other areas. He contributed to the area of programming language design as a member of the Modula-3 committee. In distributed systems he contributed to Network Objects. He made pioneering contributions with his constraint-based graphics editors (Juno and Juno-2), window systems (Trestle), optimal code generation (Denali), and multi-threaded programming (Eraser).
External links
- Greg Nelson, Memorial, Palo Alto Online (retrieved 2016-07-24)
- Greg Nelson, Posted On March 4th, 2015, Honolulu Star-Advertiser Obituaries (retrieved 2016-07-24)
- Charles Gregory Nelson: Techniques for Program Verification. Xerox Parc, 1980 (revised version of author's PhD thesis). http://people.eecs.berkeley.edu/~necula/Papers/nelson-thesis.pdf
- Herbrand Award web Page with a section devoted to the 2013 award given to Charles Gregory Nelson [1]