📄 http:^^www.cs.utexas.edu^users^boyer^students.html
字号:
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
<HTML><HEAD><TITLE>Ph. D. Students</TITLE></HEAD><BODY bgcolor="ffffff"><BODY><h3>Ph. D. Students:</h3><P>All degrees were in computer sciences unless noted "mathematics".Co-supervisors names are given in parentheses. All degrees wereawarded by the University of Texas at Austin (UT). All UTdissertations are available for inspection at the PCL library on theUT campus and may also be purchased from University Microfilms, 300N. Zeeb Road, Ann Arbor, Michigan 41806, for approximately $30.00.<ul><li> Shang-Ching Chou, <em>Proving and discovering geometry theoremsusing Wu's method</em>, 1985, mathematics (J Moore). Published as thebook <em>Mechanical geometry theorem proving</em>, D. Reidel, 1988.chou@cs.twsu.edu<li> Warren Alva Hunt, <em>FM8501 : a verified microprocessor</em>,1985, (J Moore). Published as the book <em>FM8501: A verifiedmicroprocessor</em>, Springer-Verlag LNCS 795, 1994. hunt@cli.com<li> Natarajan Shankar, <em>Proof-checking metamathematics</em>, 1986(J Moore). A version published as <em>Metamathematics, machines, andG鰀el's proof</em>, Cambridge University Press, 1994. shankar@csl.sri.com<li> Myung Won Kim, <em>On automatically generating and using examplesin a computational logic system</em>, 1986 (J Moore).<li> William D. Young, <a href="young-diss.ps.Z"> <em>A verified codegenerator for a subset of Gypsy</em></a>, 1987 (JMoore). young@cli.com<li> William R. Bevier, <em>A verified operating system kernel</em>,1987 (J Moore). The <a href="kit.ps.Z"><em>dissertation</em>,</a> minus someappendices, which may be found as examples in the <ahref="./publications.html#nqthm">Nqthm</a> distribution.bevier@cli.com<li> James Daniel Christian, <em>High-performance permutativecompletion</em>, 1989 (Dallas Lankford). jimc@lim.com<li> <a href="http://www.itd.nrl.navy.mil/ITD/5540/personnel/goldschlag/main.html">David Moshe Goldschlag</a>, <em><a href="dmg-dissertation.ps.Z">Mechanically verifying concurrentprograms</a></em>, 1992 (J Moore). goldschlag@itd.nrl.navy.mil<li> Arthur David Flatau, <em>A verified implementation of anapplicative language with dynamic storage allocation</em>, 1992 (JMoore). The <a href="cli-tr-083.ps.Z"><em>dissertation</em>,</a> minus someappendices, which may be found as examples in the <ahref="./publications.html#nqthm">Nqthm</a> distribution. flatau@lagrange.amd.com<li> Yuan Yu, <em><ahref="ftp://ftp.cs.utexas.edu/pub/techreports/tr93-09.ps.Z"> Automatedproofs of object code for a widely used microprocessor</a></em>, 1992,mathematics. A revised version to appear in Springer'sLNCS. yuanyu@src.dec.com<li> Nicholas Freitag McPhee, <em>Mechanically proving geometrytheorems using Wu's method and Collins' method</em>, 1993 (S. Chou).mcphee@cda.mrs.umn.edu<li> Sakthikumar Subramanian, <em><a href="sakthi-diss-single-spaced.ps.Z">A mechanized framework forspecifying problem domains and verifying plans</a></em>, 1993.sakthi@ba.tis.com<li> Robert Lawrence Akers, <em>Strong static type checking forfunctional Common LISP</em>, 1994 (J Moore). akers@lapaz.scicomp.com<li> Matthew Michael Wilding, <em><ahref="ftp://ftp.cs.utexas.edu/pub/boyer/wilding-diss.ps.gz">Machine-checkedreal-time system verification</a></em>, 1996 (A. Mok). mmwildin@cca.rockwell.com⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -