Ph. D. Students

All degrees were in computer sciences unless noted "mathematics". Co-supervisors names are given in parentheses. All degrees were awarded by the University of Texas at Austin (UT). All UT dissertations are available for inspection at the PCL library on the UT campus and may also be purchased from University Microfilms, 300 N. Zeeb Road, Ann Arbor, Michigan 41806, for approximately $30.00.

Shang-Ching Chou, Proving and discovering geometry theorems using Wu's method, 1985, mathematics (J Moore). Published as the book Mechanical geometry theorem proving, D. Reidel, 1988. chou@cs.twsu.edu
Warren Alva Hunt, FM8501 : a verified microprocessor, 1985, (J Moore). Published as the book FM8501: A verified microprocessor, Springer-Verlag LNCS 795, 1994. hunt@cs.utexas.edu
Natarajan Shankar, Proof-checking metamathematics, 1986 (J Moore). A version published as Metamathematics, machines, and Gödel's proof, Cambridge University Press, 1994. shankar@csl.sri.com
Myung Won Kim, On automatically generating and using examples in a computational logic system, 1986 (J Moore).
William D. Young, A verified code generator for a subset of Gypsy, 1987 (J Moore). wdyoung@texas.net
William R. Bevier, A verified operating system kernel, 1987 (J Moore). The dissertation, minus some appendices, which may be found as examples in the Nqthm distribution. bbevier@eti.com
James Daniel Christian, High-performance permutative completion, 1989 (Dallas Lankford). Jim_Christian@trilogy.com.
David Moshe Goldschlag, Mechanically verifying concurrent programs, 1992 (J Moore). David.Goldschlag@usi.net
Arthur David Flatau, A verified implementation of an applicative language with dynamic storage allocation, 1992 (J Moore). The dissertation, minus some appendices, which may be found as examples in the Nqthm distribution. flatau@lagrange.amd.com
Yuan Yu, Automated proofs of object code for a widely used microprocessor, 1992, mathematics. yuanbyu@microsoft.com
Nicholas Freitag McPhee, Mechanically proving geometry theorems using Wu's method and Collins' method, 1993 (S. Chou). mcphee@cda.mrs.umn.edu
Sakthikumar Subramanian, A mechanized framework for specifying problem domains and verifying plans, 1993. ssubramanian@cosinecom.com.
Robert Lawrence Akers, Strong static type checking for functional Common LISP, 1994 (J Moore). akers@lapaz.scicomp.com
Matthew Michael Wilding, Machine-checked real-time system verification, 1996 (A. Mok). Pc-Nqthm input here. mmwildin@cca.rockwell.com
Benjamin Price Shults, Discoveries and Experiments in the Automation of Mathematical Reasoning, 1997, mathematics (W. Bledsoe, L. Hines). bshults@bethel.edu
Ruben Antonio Gamboa, Mechanically Verifying Real-Valued Algorithms in ACL2, 1999. For just the text, see here. ruben@gamboas.org

N. B. The Nqthm input for the dissertation work of Hunt, Flatau, Shankar, and Yu may be found in the Nqthm distribution. The Pc-Nqthm input for the dissertation work of Goldschlag and Young may be found in the Pc-Nqthm distribution.