</head> <BODY vlink="#990099" link ="#990099", alink="#990099"> <table noborder cellpadding=0 cellspacing=0 width="100%"> <tr bgcolor="#EECCFF"> <td width="50%" align="left"> <font size=-1><i> <a href="http://www.cs.indiana.edu/classes/p415-sjoh/">CSCI P545</a> </i></font> <td width="50%" align="right"> <font size=-1><i> Fri Feb 6 12:13:03 EST 2009 © <a href="http://www.cs.indiana.edu/~sjohnson">[SDJ]</a> </i></font> </table> <H3> Resources and Readings </H3> <table width="100%"> <tr bgcolor="#EECCFF"> <td colspan=2><b>Lecture Notes and Textbooks</b> <tr valign="top"> <td width=25 align="center"><a href="post/terminology.pdf">[PDF]</a> <td> <i>Terminology.</i> Lecture notes. <tr valign="top"> <td width=25 align="center"><a href="post/complexity/complextity.pdf">[PDF]</a> <td> <i>Complexity of Verification.</i> Lecture notes. <tr valign="top"> <td width=25 align="center"> <a href="readings/IRP/irp.pdf">[PDF]</a> <td> Steven D. Johnson. <i>Induction, Recursion and Programming</i>. Draft textbook. Topics in Chapters 4, <b>7</b>, 9, & <b>10</b> are the most relevant to this course. <tr bgcolor="#EECCFF"> <td colspan=2><b>PVS</b> <tr valign="top"> <td width=25 align="center"><a href="http://pvs.csl.sri.com/">[HTM]</a> <td> PVS home page</a></em> <tr valign="top"> <td width=25 align="center"> <a href="readings/pvs/pvs-language-reference.pdf">[PDF]</a> <td> <i>PVS Language Reference</i> <tr valign="top"> <td width=25 align="center"> <a href="readings/pvs/pvs-prover-guide.pdf">[PDF]</a> <td> <i>PVS Prover Guide</i> <tr valign="top"> <td width=25 align="center"> <a href="readings/pvs/pvs-system-guide.pdf">[PDF]</a> <td> <i>PVS System Guide</i> <tr valign="top"> <td width=25 align="center"> <a href="readings/pvs/pvs-system-guide.pdf">[PDF]</a> <td> <i>PVS Reference Card</i>. Summarizes PVS language, Prover and System commands, keyboard shortcuts. <tr valign="top"> <td width=25 align="center"> <a href="readings/pvs/pvs-adts.pdf">[PDF]</a> <td> S. Owre and N. Shankar. <i>Abstract Datatypes in PVS</i>. Includes an extended example of Ordered Binary Trees. <tr valign="top"> <td width=25 align="center"> <a href="readings/pvs/pvs-tutorial.pdf">[PDF]</a> <td> S. Crow, et al. <i>A Tutorial Introduction to PVS.</i> First presented at the 1995 WIFT workshop. <tr valign="top"> <td width=25 align="center"> <a href="http://www.labri.fr/Perso/~gloess/imperative/">[HTM]</a> <td> Paul Y Gloess. <i> Imperative Program Verification in PVS.</i>, École nationale supérieure d'Électronique et de radioélectricité de Bordeaux, (June 14, 1999, rev. November 29, 1999). Embedding of a simple statement-oriented programming language and Hoare/Dijkstra style calculus in PVS. <tr valign="top"> <td width=25 align="center"> <a href="http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS2-library/pvslib.html">[HTM]</a> <td>Brief Summary Of NASA LaRC PVS Libraries (For PVS 2.3) Strategies developed for projects at NASA/Langley and ICASE. <tr bgcolor="#EECCFF"> <td colspan=2><b>SMV</b> <tr valign="top"> <td width=25 align="center"> <a href="readings/smv/SMVmanual.pdf">[PDF]</a> <td> <i>SMV Manual</i> <tr valign="top"> <td width=25 align="center"> <a href="http://www.cs.cmu.edu/~modelcheck/smv.html">[HTM]</a> <td> SMV home page <tr valign="top"> <td width=25 align="center"> <a href="http://patterns.projects.cis.ksu.edu/">[HTM]</a> <td> <i>Spec Patterns</i>. Model checking specification pattern repository. pattern repository</a>. A catalog of patterns showing how to express useful system properties in various temporal logics, including CTL. <tr bgcolor="#EECCFF"> <td colspan=2><b>Accidents</b> (investigate and present for extra credit) <tr valign="top"> <td width=25 align="center"><a href="http://en.wikipedia.org/wiki/Northeast_Blackout_of_2003">[HTM]</a> <td> <i>2003 Northeast Grid Failure</i> <tr valign="top"> <td width=25 align="center"><a href="http://gizmodo.com/5121822/official-fix-for-the-zune-30-fail">[HTM]</a> <td> <i>Zune 30 Failure.</i> "Microsoft responded to the Zune 30GB failure, blaming a leap-year handling bug. And they've provided a fix. Which is to wait til New Years, when the bug will go away by itself. ..." <tr bgcolor="#EECCFF"> <td colspan=2><b>Articles &etc</b> <tr valign="top"> <td width=25 align="center"><a href="http://www.cse.buffalo.edu/~rapaport/510/canprogsbeverified.html">[HTM]</a> <td> William J. Rapaport. <i>Can Programs Be Verified?</i> A bibliography of seminal articles and philisophical essays on program verification. <tr valign="top"> <td width=25 align="center"><a href="http://catless.ncl.ac.uk/Risks/">[HTM]</a> <td><i>The Risks Digest</i>. A repository of short reports on computer related risks is moderated by Peter G. Neumann at SRI's Computer Systems Lab. Not all (in fact, only some) of the material involves issues of design errors. The moderated newsgroup <tt>comp.risks</tt> <a href="news:comp.risks">[NEWS}</a> contains current risk issues under discussion. <tr bgcolor="#EECCFF"> <td colspan=2><b>Hub Pages</b> <tr valign="top"> <td width=25 align="center"><a href="http://www.cs.indiana.edu/formal-methods-education">[HTM]</a> <td> <i>Formal Methods Educational Resources</i> <tr valign="top"> <td width=25 align="center"><a href="http://www.csl.sri.com/fm.html">[HTM]</a> <td>SRI Formal Methods and Dependable Systems <tr valign="top"> <td width=25 align="center"><a href="http://www.csr.ncl.ac.uk/projects/FME/index.html">[HTM]</a> <td>Formal Methods Europe (FME) home page <tr valign="top"> <td width=25 align="center"><a href="http://www.comlab.ox.ac.uk/archive/formal-methods.html">[HTM]</a> <td>Oxford formal methods archive <tr valign="top"> <td width=25 align="center"><a href="http://www.cs.bris.ac.uk/~dattani/safety.html">]HTM]</a> <td>Safety-Critical Systems </table> </body> </html>