CS5232: Formal Specification and Design Techniques (Spring 2023)

Syllabus and Grading





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

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.