Charles Gregory Nelson (27 March 1953 – 2 February 2015) was an American computer scientist.
He lived in Juneau, Alaska for a year before settling permanently in the San Francisco Bay Area.
His thesis, Techniques for Program Verification,[3] influenced both program verification and automated theorem proving, especially in the area now named 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:[4] 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 developing the Simplify theorem prover used by ESC/Java.
He made pioneering contributions with his constraint-based graphics editors (Juno and Juno-2), windowing system (Trestle), optimal code generation (Denali), and multi-threaded programming (Eraser).