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

Schedule

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	Quiz 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 Objects with Representation Sets
April 5	Quiz 2 Project Presentations
April 12	Project Presentations

Final Projects

• Adi Herwana, Wei Letong: Formal Specification and Verification of the CSR matrix data structure in Dafny

• Li Jiate: Formal Specification and Verification of the B+ tree structure in Dafny

• Muhammad Amir, Tan Yu Wei: Formalizing the Chubby lock service with TLA+

• Wu Zhenghao, Yu Xiaoxue: Verifying LFU Algorithm with Dafny

• Ramachandran Sandhya, Tan Yee Jian: Formal Specification and Verification of the Rope data structure in Dafny

• Yuxi Ling: Enumerative Program Synthesis for ROP Exploits with SMT

• Vladimir Gladstein, Abitamim Bharmal: Verifying Sparse Matrix Multiplication with Dafny and Coq

• Gaurav Gandhi, Lim Ngian Xin Terry: Formalisation and Specification Design of Fast Paxos Algorithm in TLA+

• Anandakrishnan Venugopal, Bryan Lim: Solving a Jane Street Puzzle with Z3

• Robin Ng Geon Woo, Achmad Yogi Prakoso: Formal Specification and Verification of the Treap data structure in Dafny

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.

Copyright

Most of the lecture materials for this course are adapted, with permission, from similar classes developed by Cesare Tinelli (University of Iowa), Sarah Winkler (Free University of Bozen-Bolzano), Peter Müller (ETH Zurich), and Nadia Polikarpova (UC San Diego). The linked above slide decks contain, whenever required, respective copyright clauses.