MIME-Version: 1.0
Server: CERN/3.0
Date: Tuesday, 07-Jan-97 15:19:57 GMT
Content-Type: text/html
Content-Length: 3320
Last-Modified: Tuesday, 27-Aug-96 20:24:34 GMT
Ph. D. Students
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@cli.com
- 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). young@cli.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.
bevier@cli.com
- James Daniel Christian, High-performance permutative
completion, 1989 (Dallas Lankford). jimc@lim.com
-
David Moshe Goldschlag,
Mechanically verifying concurrent
programs, 1992 (J Moore). goldschlag@itd.nrl.navy.mil
- 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. A revised version to appear in Springer's
LNCS. yuanyu@src.dec.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.
sakthi@ba.tis.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). mmwildin@cca.rockwell.com