CS 477: Formal Software Development Methods
Video of class lectures

Lecture Schedule for Spring 2018
Schedule subject to change as course progresses.
Lecture slides for not yet given lectures are preliminary, and may change.
Jan 17 Course Introduction slides (full sized PDF) (6 up PDF)
Jan 19 Review of Propositional Logic slides (full sized PDF) (6 up PDF)
 
Jan 24 Proof Theory for Propositional Logic slides (full sized PDF) (6 up PDF)
Jan 26 Soundness of Propositional Proofs slides (full sized PDF) (6 up PDF) (annotated slides PDF)
 
Jan 31 Intro to BDDs slides (full sized PDF) (6 up PDF)
Feb 2 Construction of BDDs slides slides (full sized PDF) (6 up PDF) (annotated slides)
 
Feb 7 Introduction to Isabelle slides (full sized PDF), (6 up PDF)
theory files my_theory.thy
Feb 9 Functional Programming in Isabelle (full sized PDF), (6 up PDF)
theory files boolexp.thy
 
Feb 14 First Order Logic slides (full sized PDF) (6 up PDF)
Feb 16 First Order Logic - Proofs slides cont from last class
 
Feb 21 First Order Logic Proof slides (full sized PDF) (6 up PDF)
Feb 23 Hoare Logic (cont) slides (full sized PDF), (6 up PDF)
 
Feb 28 Hoare Logic in Isabelle slides (full sized PDF) (6 up PDF) theory files Hoare_SIMP.thy Hoare_int_data.thy Hoare_ex.thy
Mar 2 Hoare Logic in Isabelle slides from last class, theory files Hoare_SIMP.thy Hoare_int_data.thy Hoare_example.thy
 
Mar 7 Verification Condition Generation slides (full sized PDF) (6 up PDF) theory files Hoare_ann_SIMP.thy Hoare_ann_ex.thy
Mar 9 MIDTERM, EOH
 
Mar 14 Verification Condition Generation, Operational Semantics slides (full sized PDF) (6 up PDF)
Mar 16 Transition Semantics, Labeled Transition Systems slides(full sized PDF) (6 up PDF)
 
Mar 21 Spring Break
Mar 23 Spring Break
 
Mar 28 Transition Sementics, Labled Transition Systems slides(full sized PDF) (6 up PDF)
Mar 30 Labled Transition Systems, Intro to Linear Temporal Logic (LTL) slides slides (full sized PDF) (6 up PDF)
 
Apr 4 Linear Temporal Logic slides (Full PDF) (Six Up PDF)
Apr 6 Introduction to SPIN slides (Full PDF) (Six Up PDF)
 
Apr 11 Promela Syntax slides (Full PDF) (Six Up PDF)
Apr 13 Introduction to Executing SPIN slides (Full PDF) (Six Up PDF)
 
Apr 18 LTL and SPIN Verification slides (Full PDF) (Six Up PDF)
Apr 20 Abstract Interpretation slides (Full PDF) (Six Up PDF)
 
Apr 25 CFG Standard Interpretation and Abstract Interpretation slides (Full PDF) (Six Up PDF)
Apr 27 Calculating Abstract Interpretations slides (Full PDF) (Six Up PDF)
 
May 2 Abstract Interpretation slides continued
 
May 10 FINAL TBA