Practical Formal Methods (November 2024)¶
Instructor: Ilya Sergey
Lectures: 17-23 November 2024
Location: Neapolis University Pafos
Syllabus and Grading¶
Tentative Schedule¶
The course is structured as six lectures, each taking about 2.5-3 hours, including discussion and Q&A.
The exact timetable will be announced later.
Lecture |
Topics |
Materials |
|---|---|---|
1 |
Course introduction and administration Introductory case studies in TLA+, Z3, and Dafny |
|
2 |
TLA+: Basics, State Machines Specification of Transaction Commit |
|
3 |
TLA+: Commit Implementations TLA+: Specifications in Temporal Logic Fairness and Liveness |
|
4 |
SMT: Satisfiability Modulo Theories Dafny: Introduction |
|
5 |
Floyd-Hoare Logic Dafny: Reasoning about Loops and Iteration |
|
6 |
Dafny: Programs with Arrays and Objects |
Software Prerequisites¶
Please, make sure to install Visual Studio Code and the following extensions and tools:
Python 3
Dafny extension for VSCode (installing it will also install .NET and Dafny verifier)
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.
Recommended Reading¶
Leslie Lamport, The TLA+ Hyperbook.
Leslie Lamport, Specifiying Systems. 2002
K. Rustan M. Leino, Program Proofs, 2023. Preprint available here.
Copyright¶
Some of the lecture materials for this course are adapted, with permission, from the lecture material developed by
Leslie Lamport (Microsoft)
Peter Müller (ETH Zürich)
Nadia Polikarpova (UC San Diego)
Cesare Tinelli (University of Iowa)
The linked above slide decks contain, whenever required, respective copyright clauses.