Only few of the electronic lecture notes are available here, most
are on blackboard.
| Date |
Topic |
Lectures |
Assignments |
|
Feb. 29
|
Introduction
|
LEC: introduction;
Basic set theory;
Context-free grammars;
Principal of induction;
Read: background;
grammars;
induction
|
Lab 1: Software setup
DDL: Mar. 8
|
|
Mar. 21
|
Propositional logic
Constructive logic
|
LEC: Syntax;
Natural deduction;
Semantics (truth table, Boolean algebra);
Soundness and completeness;
(prop-notes |
cons-notes)
Read:
propositional logic;
constructive logic
|
Lab 2: Proof engineering
DDL: Mar. 31
|
|
Mar. 28
|
SAT
|
LEC: Normal form;
Resolution;
DPLL;
(notes)
Read: SAT
|
Lab 3: SAT
DDL: Apr. 7
|
|
Apr. 11
|
Predicate logic
|
LEC: Syntax;
Natural deduction;
Semantics;
Soundness and completeness;
(notes)
Read: predicate logic
|
|
|
Apr. 18
|
EUF theory
|
LEC: Theories;
Equality;
uninterpreted functions;
(notes)
Read: EUF theory
|
Lab 4: Theory for EUF
DDL: May. 19
|
|
Apr. 25
|
Linear arithmetic
|
LEC: Syntax;
Fourier-Motzkin;
Simplex;
Branch and Bound;
(notes)
Read: Linear arithmetic
|
Lab 5: Linear arithmetic
DDL: May. 19
|
|
May. 2
|
No class
|
Happy Labor Day!
|
|
|
May. 9
|
No class
|
Internship recruitment week
|
|
|
May. 16
|
Recitation II
|
|
|
|
May. 23
|
Theories for
data structures I
|
LEC:
Bit vectors ;
Arrays ;
Read: Bit vectors
Arrays
|
Lab 6: Theories for Data Structures
|
|
TBA
|
Theories for
data structures II
|
LEC: Pointers (notes)
Read: Pointers
|
|
|
TBA
|
Theory combination
|
LEC: Theory combination;
Nelson-Oppen;
DPLL(T);
(notes)
Read: Theory combination;
DPLL(T)
|
|
|
TBA
|
Symbolic execution
|
LEC: Operational semantics; (notes)
Path condition;
Symbolic execution; (notes)
Concolic execution; (notes)
Read: Operational semantics;
Survey of symbolic execution;
DART
|
Lab 7: Symbolic execution
|
|
TBA
|
Verification
|
LEC: Hoare triple;
Axiomatic semantics; (notes)
VC generation; (notes)
Read: Hoare logic;
Proof-Carrying Code
|
Lab 8: Hoare logic
|
|
TBA
|
Program synthesis
|
LEC: Program synthesis (notes)
Read: TBA
|
Lab 9: Program synthesis
|
|
TBA
|
Recitation I
|
LEC: Course review
Read: TBA
|
|
|
TBA
|
Recitation II
|
LEC: Course review
Read: TBA
|
|
|
TBA
|
Final test
|
Open book, open notes;
no electronic devices.
Good luck!
|
|