CS 477: Formal Software Development Methods
main
::
policy
::
lectures
::
mps
::
exams
::
unit project
:: resources ::
faq
FOLDOC
Free On-Line Dictionary of Computing
You can find just about any computing term here.
Even the ones we talk about.
Class Newsgroup
https://piazza.com/class#spring2014/cs477">Piazza class newsgroup
Passwords & EWS
Learn about netids and passwords
EWS
The on-line EWS manual
Lab reservations
Change EWS Password
EWS Print
Related Papers
Propositional Logic
Verification Conditions for Source-level Imperative Programs
Explaining Verification Conditions
Ken McMillan's Thesis: Symbolic Model Checking
A tutorial on model checking with an example analysis of the Needham-Schroeder public key protocol.
Software
Isabelle Theorem Prover
Main Isabelle website
Local copies of downloads for Isabelle2012
Isabelle2012 for 64-bit Linux
Isabelle2012 for Windows
Isabelle2012 for Mac OS X
Postscript/PDF Viewers
Ghostview
(PS and PDF)
Adobe Acrobat Reader
(PDF only)
Xpdf
(PDF only)