📄 http:^^www.cs.utexas.edu^users^boyer^courses^cs395t-spring96.html
字号:
MIME-Version: 1.0
Server: CERN/3.0
Date: Monday, 06-Jan-97 21:39:25 GMT
Content-Type: text/html
Content-Length: 3826
Last-Modified: Tuesday, 16-Apr-96 18:41:34 GMT
<HTML><HEAD><TITLE>CS 395T and PHL 391</TITLE></HEAD><BODY bgcolor="ffffff"><BODY><h2>CS 395T and PHL 391, Spring 1996, <em>Foundations ofMathematics</em>, TT 2:00-3:30, Taylor 3.144</h2><UL><LI> Course blurb: There are many approaches to formal reasoning. Theobjective of specifying computer programs, including the formalizationof worlds with which programs are to interact, has led to the creationof numerous tools for formal reasoning. We will examine some systemsfor formal reasoning while examining a number of mechanical formalmethods tools that support these different systems. Examples of suchsystem/tool pairs are: <p> <pre> System Tool Primitive Recursive Arithmetic Boyer-Moore Prover, ACL2 First Order Logic Otter, Nelson's qed Higher Order Logic HOL, IMPS Equational Reasoning OBJ Set Theory Mizar, Quaife/Otter, PVS Type Theory NuPrl, Lego, Coq</pre><p>Students will choose, with the help of the instructor, a system and/ortool to examine and the grade will be based upon presentations aboutthese.<p><LI><!WA0><a href="http://www.mcs.anl.gov/qed/index.html"> The QED Project</a><UL><LI>HTML Version of <!WA1><ahref="http://www.cybercom.net/~rbjones/rbjpub/logic/qedres00.htm">theQED Manifesto</a><LI>Plain text version of <!WA2><ahref="ftp://ftp.cs.utexas.edu/pub/boyer/qed-manifesto">the QEDManifesto</a></UL><p><LI><!WA3><a href="http://www.comlab.ox.ac.uk/archive/formal-methods.html">Bowen' Formal Methods Web Page</a> and a <!WA4><a href="http://www.cs.utexas.edu/users/boyer/courses/backup-formal-methods.html">backup copy</a>.<p><LI>The chief assignment. Select a formal methods system, e.g.,from Bowen's Formal Methods Web Page above, and report via in-class,oral presentations on either its logical foundations or upon its use.Many of these systems have good, freely available implementations.Consult with me before making a final choice.<p><LI>No tests, no final. Only the presentation(s).<p><LI>I hope to have a number of guest presentations from the localformal methods community.</UL><p><LI>*Very* Tentative Schedule<UL><! Jan 30 -- Matt Wilding on Nqthm proofs about the Clinc Stack andthe Nim program Feb 1 -- Matt Wilding on Nqthm proofs about real time programs Feb 6 -- Carl Pixley (Motorola) Formal Verification of Hardware:Hardware Models; CTL Language; BDD implementation of model checking;Industrial use: Abstract modelling, Implementation modellingFeb 8 -- J Moore (Computational Logic) Overview of ACL2 andits relationship to Common LispFeb 13 -- Matt Kaufmann (Motorola) Tutorial examples of ACL2 useFeb 15 -- J Moore (Computational Logic) Advanced ACL2 applicationsFeb 20 -- Strongly urge attendance at an Ed Clarke talk this week(He will be giving a talk on Monday, Feb. 19th in Taylor 3.128 from2:00-3:00 and on Wednesday, Feb. 21st in Taylor 3.128 from 1:30-2:30.)Feb 22 -- Warren Hunt (Computational Logic) FM9001 VerificationFeb 27 -- Warren Hunt (Computational Logic) FM9001 VerificationFeb 29 -- Jun SawadaMarch 5 -- Matt WildingMarch 7 -- Ruben GamboaMarch 12 -- Spring BreakMarch 14 -- Spring BreakMarch 19 -- Jun Sawada continuesMarch 21 -- Carl Pixley (Motorola) CTLMarch 26 -- Markus KaltenbachMarch 28 -- Kenneth Chen -- OtterApril 2 -- Patrick Ray -- LarchApril 4 -- Larry Hines (UT and EDS) -- A set theory proverApril 9 -- William Adams -- Type theoryApril 11 -- Rick Tanney -- Coq><LI> April 16 -- Rick Tanney -- Coq continued<LI> April 18 -- Trevor Hicks -- Otter<LI> April 23 -- Ruben Gamboa on ACL2 and Square root of 2<LI> April 25 -- Samuel Guyer -- Circal and process algebras<LI> April 30 -- Sawada -- PVS<LI> May 2 -- Russell Turpin (SES) -- Galois</UL>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -