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 |
|