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
March 12	Introduction	LEC: introduction; Basic set theory; Context-free grammars; Principal of induction; Read: set theory; grammars; induction	Assignment 1: software setup
March 19	Propositional logic	LEC: Syntax; Natural deduction; Semantics (truth table, Boolean algebra); Soundness and completeness; (notes) Read: propositional logic
March 26	Constructive logic	LEC: Syntax; Natural deduction; Semantics; Soundness and completeness; (notes) Read: constructive logic	Assignment 2: Proof engineering
April 2	Recitation 1	LEC: Course review; Coq usage; Assignment 1, 2; (notes)
April 9	SAT	LEC: Normal form; Resolution; DPLL; (notes) Read: SAT	Assignment 3: SAT
April 16	Predicate logic	LEC: Syntax; natural deduction; Semantics; soundness and completeness; (notes) Read: predicate logic	Assignment 4: Proof for predicate logic
April 23	EUF theory	LEC: Theories; Equality; uninterpreted functions; (notes) Read: EUF theory	Assignment 5: Theory for EUF
April 30	Linear arithmetic	LEC: Syntax; Fourier-Motzkin; Simplex; Branch and Bound; (notes) Read: linear arithmetic	Assignment 6: Linear arithmetic
May 14	No class	Recruiting week, good luck!
May 21	Recitation 2	LEC: Course review; More practice; Assignment 3, 4, 5; (notes)
May 29	Middle test	Open book, open notes, no electronic devices.
May 29	Theories for data structures	LEC: Bit vectors; (notes) Arrays; (notes) Pointers; (notes) Read: Bit vectors Read: Arrays Read: Pointers
June 5	Theory combination; DPLL(T)	LEC: Theory combination; Nelson-Oppen; (notes) DPLL(T); (notes) Read: Theory combination Read: DPLL(T)	Assignment 7: Theories for Data Structures
June 12	Recitation 3	LEC: Middle test review; Course review; Assignment 6, 7; (notes)
June 19	Symbolic execution	LEC: Operational semantics; (notes) Path condition; Symbolic execution; (notes) Concolic execution; (notes) Read: Operational semantics Read: Survey of symbolic execution Read: DART	Assignment 8: Symbolic execution
June 26	Verification	LEC: Hoare triple; Axiomatic semantics; (notes) VC generation; (notes) Read: Hoare logic Read: Proof-Carrying Code	Assignment 9: Hoare logic
July 3	Program analysis	LEC: Program analysis Read: TBA
July 10	Program synthesis	LEC: Program synthesis Read: TBA
July 21	Final test	14:00--16:00pm. Open book, open notes; no electronic devices. Good luck!