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.

TBA: To Be Announced.


Date Topic Lectures Assignments
Sep. 7 Introduction LEC: introduction;
Basic set theory;
Context-free grammars;
Principal of induction;

Code: set code;
relation code;
function code;
subset sum code;
grammar code;
induction code;

Read: set;
grammars;
induction; 		Lab 1: Software setup
DDL: Sep. 21
Sep. 8 Propositional logic; Constructive logic LEC: Syntax;
Natural deduction;
Semantics (truth table, Boolean algebra);
Soundness and completeness;
proposition notes;
constructive notes;

Code: truth table code;

Read: propositional logic;
constructive logic 		Lab 2: Proof engineering
DDL: Sep. 22
Sep. 14 SAT LEC: Normal form;
Resolution;
DPLL;
(notes)

Code: subset sum problem;
knapsack problem;
n-queen problem;

Read: SAT 		Lab 3: SAT
DDL: Sep. 28
Sep. 15 Predicate logic LEC: Syntax;
Natural deduction;
Semantics;
Soundness and completeness;
(notes)

Code: deduction code;

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

Code: connectivity code

Read: EUF theory 		Lab 4: Theory for EUF
DDL: Oct. 12
Sep. 22 Recitation I notes: notes
Sep. 28 Linear arithmetic LEC: Syntax;
Fourier-Motzkin;
Simplex;
Branch and Bound;
(notes)

Code: geometry
non linear
IMO problems
Sudoku problem

Read: Linear arithmetic 		Lab 5: Linear arithmetic
DDL: Oct. 12
Sep. 29 Theories for
data structures I 		LEC: Bit vectors;
Arrays;

Read: Bit vectors
Arrays
Lab 6: Theories for Data Structures
DDL: Oct. 13
Oct. 12 Theories for
data structures II 		LEC: Pointers (notes)

Read: Pointers
Oct. 13 Recitation II notes: notes
Oct. 19 Theory combination
 LEC: Theory combination;
DPLL(T);

Read: Theory combination ;
DPLL(T)
Oct. 20 Symbolic execution LEC: Symbolic execution ;
Concolic execution;

Read: Survey of symbolic execution ;
DART 		Lab 7: Symbolic execution
DDL: Nov. 3
Oct. 26 Verification LEC: Hoare triple ;
Axiomatic semantics;
VC generation ;

Code: Verus code;

Read: Hoare logic ;
Proof-Carrying Code 		Lab 8: Hoare logic
DDL: Nov. 10
Oct. 27 Program synthesis LEC: Program synthesis (notes)

Read: TBA
Nov. 2 Recitation III notes: notes
TBA Final test Location: TBA

Open book, open notes;
no electronic devices.

Good luck!