Formal Methods Foundation

Schedule

Only few of the electronic lecture notes are available here, most are on blackboard.

This schedule is tentative and subject to change at any time.


Date Topic Lectures Assignments
Feb. 27 Introduction LEC: introduction;
Basic set theory;
Context-free grammars;
Principal of induction;
(powerset code)
(grammar code)

Read: background;
grammars;
induction
Lab 1: Software setup
DDL: Mar. 13
Mar. 6 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. 20
Mar. 13 SAT LEC: Normal form;
Resolution;
DPLL;
(notes)
(subset sum code)
(knapsack code)
(n-queen code)

Read: SAT
Lab 3: SAT
DDL: Mar. 27
Mar. 20 Recitation I notes: notes
Mar. 27 Predicate logic LEC: Syntax;
Natural deduction;
Semantics;
Soundness and completeness;
(notes)
(deduction code)

Read: predicate logic
 
Apr. 3 EUF theory LEC: Theories;
Equality;
uninterpreted functions;
(notes)
(connectivity code)

Read: EUF theory
Lab 4: Theory for EUF
Apr. 10 Linear arithmetic LEC: Syntax;
Fourier-Motzkin;
Simplex;
Branch and Bound;
(notes)

Read: Linear arithmetic
Lab 5: Linear arithmetic
Apr. 17 Recitation II notes: TBA
Apr. 24 Theories for
data structures I
LEC: Bit vectors;
Arrays;

Read: Bit vectors
Arrays
Lab 6: Theories for Data Structures
May. 1 No class Happy Labor Day!
May. 22 Theories for
data structures II
LEC: Pointers (notes)

Read: Pointers
May. 29 Theory combination
LEC: Theory combination;
DPLL(T);

Read: Theory combination ;
DPLL(T)
Jun. 5 Symbolic execution LEC: Operational semantics ;
Path condition;
Symbolic execution ;
Concolic execution;

Read: Operational semantics ;
Survey of symbolic execution ;
DART
Lab 7: Symbolic execution
Jun. 12 Verification LEC: Hoare triple ;
Axiomatic semantics;
VC generation ;
Verus example;

Read: Hoare logic ;
Proof-Carrying Code
Lab 8: Hoare logic
Jun. 19 Program synthesis LEC: Program synthesis (notes)

Read: TBA
Lab 9: Program synthesis
Jun. 26 Recitation III notes: TBA
TBA Final test Location: TBA

Open book, open notes;
no electronic devices.

Good luck!