Class
|
Date
|
Topic
|
Reading
|
Handouts
|
C1
|
16/1
|
- Introduction
- Organization
|
|
|
|
|
Part I. Temporal Logic and Model Checking
|
|
|
C2
|
18/1
|
- Introduction to model checking
- Linear-time Temporal Logic (LTL)
|
|
|
C3
|
24/1
|
- LTL equivalences
- Model checking as a language inclusion problem
|
|
|
C4
|
25/1
|
- Büchi automata
- LTL model checking
|
|
|
C5
|
27/1
|
|
|
|
C6
|
30/1
|
- SPIN lab assignment presentation
- Security policies and policy enforcement
|
|
|
|
|
Part II. Hoare Logic and Program Verification
|
|
|
C7
|
31/1
|
- A core programming language
- Hoare triples
- A proof calculus for partial correctness
|
- book 4.1
- book 4.2
- book 4.3.1
|
|
C8
|
3/2
|
- Loop invariants
- Proof tableaux
- Example verifications
|
|
|
C9
|
6/2
|
- Soundness and completeness
- Automatic program verification
- Weakest preconditions
- Verification condition generation (VCG)
|
|
|
C10
|
7/2
|
- Symbolic execution
- VeriFast tutorial (Java)
|
|
|
C11
|
10/2
|
- Verifying data race freedom with VeriFast
|
|
|
|
|
Part III. Information Flow Analysis
|
|
|
C12
|
14/2
|
- VeriFast lab assignment presentation
- Introduction to information flow security
|
|
|
C13
|
17/2
|
- Introduction to type systems for information flow security
|
|
|
C14
|
21/2
|
- Taint analysis with Python library
- Information flow and type systems
|
|
|
C15
|
22/2
|
- Information flow and type systems
- Jif: Java + noninterference type system
|
|
|
C16
|
24/2
|
- End of the introduction to information flow security
|
|
|
C17
|
2/3
|
- Workshop on Information Flow Analysis
|
|
|
C18
|
5/3
|
- Workshop on Information Flow Analysis
|
|
|