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/illinois/spring2020/cs477ece478, Piazza class newsgroup
Passwords & EWS
Learn about netids and passwords
EWS
The on-line EWS manual
Lab reservations
EWS Print Services
EWS Print Quotas
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
Postscript/PDF Viewers
Ghostview
(PS and PDF)
Adobe Acrobat Reader
(PDF only)
Xpdf
(PDF only)