📄 http:^^lal.cs.byu.edu^people^black.html
字号:
Date: Tue, 14 Jan 1997 20:33:41 GMT
Server: Apache/1.0.3
Content-type: text/html
Content-length: 7757
Last-modified: Wed, 04 Dec 1996 00:47:34 GMT
<HTML><HEAD><TITLE>Home Page for Paul E. Black</TITLE><!-- describe the document, avoid context sensitive descriptions --><meta name="description" value="Biographical information about Paul Black with links to on-line copies of technical reports."><!-- keywords for the document --><meta name="keywords" value="HOL, theorem proving, BYU"><!-- should be "document" unless providing a search, then "service" --><meta name="resource-type" value="document"><!-- use global for documents to be indexed outside BYU --><meta name="distribution" value="global"></HEAD><BODY><h1>Home Page for Paul E. Black</h1><ADDRESS>Paul E. Black</ADDRESS><ADDRESS><!WA0><A HREF="http://lal.cs.byu.edu/homepage.html">Laboratory for Applied Logic</A></ADDRESS> <ADDRESS><!WA1><A HREF="http://www.cs.byu.edu/">Dept. of Computer Science</A>, <!WA2><A HREF="http://www.cs.byu.edu/building/TMCB-3rd.html">TMCB 3325</A></ADDRESS><ADDRESS><!WA3><A HREF="http://www.byu.edu/">Brigham Young University</A></ADDRESS><ADDRESS><!WA4><A HREF="http://www.cs.byu.edu/map-info/tourProvo.html">Provo</A>,<!WA5><A HREF="http://www.cs.byu.edu/tourUtah.html">Utah</A> 84602-6576</ADDRESS><P><ADDRESS><!WA6><img align=top src="http://lal.cs.byu.edu/images/phone-small.xbm" alt="telephone:"> +1 801 378 8113</ADDRESS> <ADDRESS>black@cs.byu.edu</ADDRESS><ADDRESS>p.black@ieee.org</ADDRESS><ADDRESS>KC7PKT</ADDRESS><P>Paul Black is studying at<!WA7><A HREF="http://www.byu.edu/">Brigham Young University</A>where he is pursuing a Ph.D. in Computer Science. He began his Ph.D.program at <!WA8><A HREF="http://www.berkeley.edu/">UC Berkeley</A>, andtransferred to BYU in 1993. His research interests areformal verification of software and software engineering.<P>Black earned an MS in Computer Science at the <!WA9><A HREF="http://www.cs.utah.edu/">University of Utah</A>in 1983 and a BS in Mathematics at <!WA10><A HREF="http://www.suu.edu/">Southern Utah State College</A> (nowSouthern Utah University) in 1973. Hehas 17 years industrial experience developing IC design andverification tools, designing configuration management systems,assuring software quality, and managing business data processing. Heis a student member of the <!WA11><A HREF="http://info.acm.org">ACM</A> andthe <!WA12><A HREF="http://www.ieee.org/">IEEE</A>. <P>He served a mission for the<!WA13><A HREF="http://www.lds.org/">LDS Church</a> in<!WA14><A HREF="http://www.xmission.com/~dkenison/brasil/bra_sps.html">Brazil</A>, and has visited <!WA15><A HREF="http://www.adfa.oz.au/CS/flg/col/be.html">Belgium</A>, <!WA16><A HREF="http://www.adfa.oz.au/CS/flg/col/ca.html">Canada</A>, <!WA17><A HREF="http://www.vn.fi/vn/um/">Finland</A>,<!WA18><A HREF="http://www.adfa.oz.au/CS/flg/col/de.html">Germany</A>, <!WA19><A HREF="http://www.adfa.oz.au/CS/flg/col/gb.html">Great Britain</A>, and <!WA20><A HREF="http://www.adfa.oz.au/CS/flg/col/mx.html">Mexico</A>.There's even a recent <!WA21><A HREF="http://lal.cs.byu.edu/pictures/Paul.Black.gif">picture</A> on-line.He keeps favorite links in a<!WA22><A HREF="http://lal.cs.byu.edu/people/black/hotlist.html">personal hotlist</A>which he updates occasionally.<HR><H2>Published Papers On-Line</H2><UL><LI><strong>Paul E. Black and Phillip J. Windley</strong>,<em>Verifying Resilient Software</em>,to be printed in the Proceedings of the<!WA23><A HREF="http://www.cba.hawaii.edu/hicss/">Thirtieth Hawai`i International Conference on on System Sciences(HICSS-30)</A>, January 1997.<!WA24><A HREF="http://lal.cs.byu.edu/people/black/Papers/hicss30.dvi">DVI</A> (36 kb) and<!WA25><A HREF="http://lal.cs.byu.edu/people/black/Papers/hicss30.ps">Postscript</A> (123 kb).<LI><strong>Paul E. Black and Phillip J. Windley</strong>,<em>Inference Rules for Programming Languages with Side Effects inExpressions</em>,<!WA26><A HREF="http://www.abo.fi/~jharriso/TPHOLs96.html">Theorem Proving in Higher Order Logics:9th International Conference, (TPHOLs '96)</A>,edited by Joakim von Wright, Jim Grundy, and John Harrison,Springer-Verlag, Berlin, Germany, 1996, pp. 51-60.<!WA27><A HREF="http://lal.cs.byu.edu/people/black/Papers/hol96.dvi">DVI</A> (34 kb) and<!WA28><A HREF="http://lal.cs.byu.edu/people/black/Papers/hol96.ps">Postscript</A> (128 kb).<LI><strong>Paul E. Black, Kelly M. Hall, Michael D. Jones, TrentN. Larson, and Phillip J. Windley</strong>, <em>A Brief Introduction to Formal Methods</em>,Proceedings of the IEEE 1996 Custom Integrated Circuits Conference, SanDiego, California, May 1996. <!WA29><A HREF="http://lal.cs.byu.edu/people/black/Papers/formMeth.ps">Postscript</A> (96 kb).<LI><strong>Paul E. Black and Phillip J. Windley</strong>,<em>Automatically Synthesized Term Denotation Predicates: A Proof Aid</em>,<!WA30><A HREF="http://lal.cs.byu.edu/lal/hol95/hol95.html">Higher Order Logic Theorem Proving and Its Applications (HOL '95)</A>, edited by E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss,Springer-Verlag, Berlin, Germany, 1995, pp. 46-57.<!WA31><A HREF="http://lal.cs.byu.edu/people/black/Papers/hol95.ps">Postscript</A> (120 kb).<LI><strong>Mor Harchol-Balter and Paul E. Black</strong>,<em>Queuing Analysis of Oblivious Packet-Routing Networks</em>,5th ACM/<!WA32><A HREF="http://www.siam.org/">SIAM</a> Symposium on DiscreteAlgorithms (SODA '94), Washington, D.C., (January 1994), ACM, pp. 583 - 592. <!WA33><A HREF="http://lal.cs.byu.edu/people/black/Papers/soda.ps">Postscript</A> (190 kb). Expanded version with application to tori in<!WA34><A HREF="http://lal.cs.byu.edu/people/black/Papers/extension.ps">Postscript</A> (203 kb).</UL><H2>Finished Projects</H2><UL><LI>I taught <!WA35><A HREF="http://lal.cs.byu.edu/cs130">ScientificProgramming - C</a>.<LI>Notes on my lecture to the Software Engineering course on<!WA36><a href="http://lal.cs.byu.edu/people/black/cs327.chap9.html">Formal Methods</a><LI><!WA37><A HREF="http://lal.cs.byu.edu/people/black/universe.html">On theComposition of the Universe</A><LI>The Orbiter<!WA38><A HREF="http://lal.cs.byu.edu/people/black/shuttle.html">Discovery'sVisit to Utah</A>.</UL><H3>Other, Less Directed Links</H3><P>I've put together some web sites and collections. Hereare some I'm especially happy with and links to other miscellaneouson-line stuff of mine.<UL><LI>The<!WA39><A HREF="http://lal.cs.byu.edu/people/black/dickinson.html">Emily Dickinson home page</A> including an<!WA40><A HREF="http://lal.cs.byu.edu/mlists/emweb/">archive of a discussion list</A> and links to over<!WA41><A HREF="http://lal.cs.byu.edu/people/EDickinson/poemsOnline.html">370 of her poems on-line</a>.<LI>I led a group consisting of most of my OO class in building a hypertext<!WA42><A HREF="http://osm7.cs.byu.edu/OSA/tutorial.html">OSA Tutorial</A>. There are <!WA43><A HREF="http://osm7.cs.byu.edu/OSA/generalConst.html#beSpecific">links to on-line quizes</A>, but the quiz program is currently(21Mar96) not working.<LI>As an experiment in HTML graphics and interfaces, I designed somepages to resemble<!WA44><A HREF="http://www.imall.com/startrek/ncc1701d/">control panels on the Enterprise</a>.<LI>To help a professor, I put the<!WA45><A HREF="http://lal.cs.byu.edu/lalac/">Language And Learning Across Curriculum</A> Committee on line,converting their<!WA46><A HREF="http://lal.cs.byu.edu/lalac/bibliog.html">bibliography</a>,<!WA47><A HREF="http://lal.cs.byu.edu/lalac/brochure.html">brochure</a>,etc. to HTML.<LI>Learning HOL lessons.<!WA48><A HREF="http://lal.cs.byu.edu/people/black/lesson1.html">Goal Directed Proof</A> (#1),<!WA49><A HREF="http://lal.cs.byu.edu/people/black/lesson2.html">Induction</A> (#2),<!WA50><A HREF="http://lal.cs.byu.edu/people/black/lesson4.html">The Assumption List</A> (#4).</UL><HR><EM>UpdatedTue Dec 3 17:47:33 1996</EM><ADDRESS>by <!WA51><a href="http://lal.cs.byu.edu/people/black/black.html">Paul E. Black</a> (<!WA52><a href="mailto:black@lal.cs.byu.edu">black@lal.cs.byu.edu</a>)</ADDRESS></BODY></HTML>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -