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
Lectures
Date |
Topics |
Materials |
---|---|---|
January 11 |
Course introduction and administration |
|
January 18 |
Introductory case study in TLA+ |
|
January 25 |
Introductory case studies in Z3 and Dafny |
Slides from the previous week |
February 1 |
TLA+: Basics, State Machines Specification of Transaction Commit |
|
February 8 |
TLA+: Commit Implementations Paxos (Homework) |
|
February 15 |
TLA+: Specifications in Temporal Logic Fairness and Liveness, Refinement |
|
March 1 |
SAT: Boolean Satisfiability and its Applicaitons |
|
March 8 |
SMT: Satisfiability Modulo Theories |
|
March 15 |
Dafny: Introduction Floyd-Hoare Logic |
|
March 22 |
Dafny: Reasoning about Loops and Iteration |
|
March 29 |
Dafny: Programs with Arrays and Objects |
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.