Home Details Schedule Resources

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
Nov. 15 Introduction LEC: introduction;
Basic set theory;
Context-free grammars;
Principal of induction;

Read: background;
grammars;
induction 		Lab 1: Software setup
DDL: Nov. 30
Nov. 16 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: Nov. 30
Nov. 22 SAT LEC: Normal form;
Resolution;
DPLL;
(notes)

Read: SAT 		Lab 3: SAT
DDL: Dec. 7
Nov. 23 Recitation I notes: TBA
Nov. 29 Predicate logic LEC: Syntax;
Natural deduction;
Semantics;
Soundness and completeness; (notes)

Read: predicate logic 		 
Nov. 30 EUF theory LEC: Theories;
Equality;
uninterpreted functions;
(notes)

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

Read: Linear arithmetic 		Lab 5: Linear arithmetic
DDL: Dec. 28
Dec. 7 Recitation II notes: TBA
Dec. 13 Theories for
data structures I 		LEC: Bit vectors ;
Arrays ;

Read: Bit vectors
Arrays
Lab 6: Theories for Data Structures
DDL: Jan. 4
Dec. 14 Theories for
data structures II 		LEC: Pointers (notes)
Read: Pointers
Dec. 20 Theory combination
 LEC: Theory combination;
DPLL(T);

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

Read: Operational semantics ;
Survey of symbolic execution ;
DART 		Lab 7: Symbolic execution
DDL: Jan. 14
Dec. 27 Verification LEC: Hoare triple ;
Axiomatic semantics;
VC generation ;
Verus example;

Read: Hoare logic ;
Proof-Carrying Code 		Lab 8: Hoare logic
DDL: Jan. 14
Dec. 28 Program synthesis LEC: Program synthesis (notes)

Read: TBA 		Lab 9: Program synthesis
Jan. 3 Recitation III notes: TBA
Jan. 4
Jan. 10 notes: 2023-2024-2 final exam
Jan. 11
Jan. 14 Final test Location: GT-B112, GT-B212

Open book, open notes;
no electronic devices.

Good luck!