|
Schedule subject to change as course progresses.
|
|
Lecture slides for not yet given lectures are
preliminary, and may change.
|
| Day |
Date |
Topic |
Slides and Code |
| 1 |
Jan 22 |
Course Introduction |
slides
(full sized PDF)
(6 up PDF)
|
| 2 |
Jan 24 |
Review of Propositional Logic |
slides
(full sized PDF)
(6 up PDF)
|
| |
|---|
| 3 |
Jan 29 |
Proof Theory for Propositional Logic |
slides
(full sized PDF)
(6 up PDF)
|
| 4 |
Jan 31 |
Soundness of Propositional Proofs |
slides
(full sized PDF)
(6 up
PDF)
|
| |
|---|
| 5 |
Feb 5 |
Intro to BDDs |
slides
(full sized PDF)
(6 up PDF)
|
| 6 |
Feb 7 |
Construction of BDDs |
slides
(full sized PDF)
(6 up PDF)
(full sized pic PDF)
(6 up pic slides)
|
| |
|---|
| 7 |
Feb 12 |
Introduction to Isabelle |
slides
(full sized PDF),
(6 up PDF)
theory files
my_theory.thy
|
| 8 |
Feb 14 |
Functional Programming in Isabelle |
slides
(full sized PDF),
(6 up PDF)
theory files
boolexp.thy
|
| |
|---|
| 9 |
Feb 19 |
First Order Logic |
slides
(full sized PDF)
(6 up PDF)
|
| 10 |
Feb 21 |
First Order Logic - Proofs |
slides cont from last class
|
| |
|---|
| 11 |
Feb 26 |
First Order Logic Proof |
slides
(full sized PDF)
(6 up PDF)
theory file
fol_example
|
| 12 |
Feb 28 |
Hoare Logic (cont) |
slides
(full sized PDF),
(6 up PDF)
|
| |
|---|
| 13 |
Mar 4 |
Hoare Logic in Isabelle |
slides
(full sized PDF)
(6 up PDF)
theory files
lifted_basics
lifted_int_predicate_logic
lifted_int_data
SIMP_syntax.thy
Hoare_SIMP.thy
Hoare_ex.thy
|
| 14 |
Mar 6 |
Hoare Logic in Isabelle |
slides from last class,
theory files
Hoare_SIMP.thy
Hoare_int_data.thy
Hoare_ex.thy
Hoare_example.thy
|
| |
|---|
| 15 |
Mar 11 |
Verification Condition Generation |
slides
(full sized PDF)
(6 up PDF)
theory files
Hoare_ann_SIMP.thy
Hoare_ann_ex.thy
|
| 16 |
Mar 13 |
Verification Condition Generation, Operational
Semantics
|
slides
(continued from Mar 11)
theory files Hoare_ex.thy
|
| |
|---|
| |
Mar 18 |
Spring Break |
|
| |
Mar 20 |
Spring Break |
|
| |
|---|
| 17 |
Mar 25 |
Natural Semantics |
slides
(full sized PDF)
(6 up
PDF)
theory
files SIMP_nat_sem.thy
Hoare_sound_and_complete.thy
|
| 18 |
Mar 27 |
Natural and Transition Sementics
|
slides
(full sized PDF)
(6 up
PDF)
|
| |
|---|
| 19 |
Apr 1 |
Labled Transition Systems |
slides
(full sized PDF)
(6 up PDF)
|
| 20 |
Apr 3 |
Linear Temporal Logic
|
slides
(Full PDF)
(Six Up PDF)
|
| |
|---|
| 21 |
Apr 8 |
Introduction to Model Checking |
slides
(Full PDF)
(Six Up PDF)
|
| 22 |
Apr 10 |
Buchi Automata |
slides
(Full PDF)
(Six Up PDF)
|
| |
|---|
| 23 |
Apr 15 |
LTL Model Checking Alg (1) |
slides
(Full PDF)
(Six Up PDF)
|
| 24 |
Apr 17 |
LTL Model Checking Alg (2) |
slides
|
| |
|---|
| 25 |
Apr 22 |
LTL and SPIN Verification |
slides
(Full PDF)
(Six Up PDF)
|
| 26 |
Apr 24 |
Abstract Interpretation |
slides
(Full PDF)
(Six Up PDF)
|
| |
|---|
| 27 |
Apr 29 |
CFG Standard Interpretation and Abstract
Interpretation
|
slides
(Full PDF)
(Six Up PDF)
|
| 28 |
May 1 |
Calculating Abstract Interpretations |
slides
(Full PDF)
(Six Up PDF)
|
| |
| 29 |
May 6 |
Abstract Interpretation |
slides continued |
| |
|---|
| |
May 12 |
FINAL 8:00am-10:00am |
|