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