CS5232: Formal Specification and Design Techniques (Spring 2023)

• Instructor: Ilya Sergey

• Lectures: Wednesdays, 10:00am-12:00pm

• Location: COM1-0212

• Teaching Assistant: George Pîrlea

Syllabus and Grading

• Course Syllabus and Policies
• Research Project: Guidelines and Deliverables

Lectures

Date	Topics	Materials
January 11	Course introduction and administration	Slides 01 Haxthausen 2010
January 18	Introductory case study in TLA+	Slides 02 Basic Examples: Code
January 25	Introductory case studies in Z3 and Dafny	Slides from the previous week Basic Examples (same): Code
February 1	TLA+: Basics, State Machines Specification of Transaction Commit	TLA+ Video Course (Parts 1-5) TLA+ Examples
February 8	TLA+: Commit Implementations Paxos (Homework)	TLA+ Video Course (Parts 5-7) Slides on consensus Consensus on Transaction Commit
February 15	TLA+: Specifications in Temporal Logic Fairness and Liveness, Refinement	TLA+ Video Course (Parts 8-10) Specifying Liveness in TLA+
March 1	SAT: Boolean Satisfiability and its Applicaitons	Slides on SAT
March 8	SMT: Satisfiability Modulo Theories	Slides on SMT SMT examples
March 15	Dafny: Introduction Floyd-Hoare Logic	Intro to Dafny (slides) Floyd-Hoare logic (slides) Dafny examples
March 22	Dafny: Reasoning about Loops and Iteration	Loops in Dafny (slides)
March 29	Dafny: Programs with Arrays and Objects	Arrays in Dafny (slides) Programs with arrays

Additional Materials

This course’s GitHub Organisation. Please, email me your GitHub handle to have access to the code from live demos and other materials.

Bibliography

• [Haxthausen 2010]: A. Haxthausen. An Introduction to Formal Methods for the Development of Safety-critical Applications. Technical report, 2010.

• Leslie Lamport, The TLA+ Hyperbook.

• Leslie Lamport, Specifiying Systems. 2002

• Daniel Kroening and Ofer Strichman, Decision Procedures: An Algorithmic Point of View, 2016.

• K. Rustan M. Leino, Program Proofs, 2023. Preprint available here.