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.
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
- 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.
- Warren Alva Hunt, FM8501 : a verified microprocessor,
1985, (J Moore). Published as the book FM8501: A verified
microprocessor, Springer-Verlag LNCS 795, 1994. email@example.com
- Natarajan Shankar, Proof-checking metamathematics, 1986
(J Moore). A version published as Metamathematics, machines, and
Gödel's proof, Cambridge University Press, 1994. firstname.lastname@example.org
- Myung Won Kim,
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). email@example.com
- 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.
- James Daniel Christian, High-performance permutative
completion, 1989 (Dallas Lankford). Jim_Christian@trilogy.com.
David Moshe Goldschlag, Mechanically
verifying concurrent programs, 1992 (J
- 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. firstname.lastname@example.org
- Yuan Yu, Automated
proofs of object code for a widely used microprocessor, 1992,
- Nicholas Freitag McPhee, Mechanically proving geometry
theorems using Wu's method and Collins' method, 1993 (S. Chou).
- Sakthikumar Subramanian, A mechanized
framework for specifying problem domains and verifying plans, 1993.
- Robert Lawrence Akers, Strong static type
checking for functional Common LISP, 1994 (J
- Matthew Michael Wilding, Machine-checked
real-time system verification, 1996 (A. Mok). Pc-Nqthm input
- Benjamin Price Shults, Discoveries and
Experiments in the Automation of Mathematical Reasoning, 1997,
mathematics (W. Bledsoe, L. Hines). email@example.com
- Ruben Antonio Gamboa, Mechanically Verifying
Real-Valued Algorithms in ACL2, 1999. For just the text,