Course · Postgraduate, 10 credits
Algorithmic Program Verification
Techniques for infinite-state model checking, with applications to weak memory models. Fifteen recorded lectures and nine slide decks.
Background
Parallel systems have become a critical part of the infrastructure of our society, through platforms such as multicores and cloud technology. Most parallel software runs on platforms that do not guarantee sequential consistency: they implement optimizations that relax inter-component synchronization, and so offer only weak consistency guarantees. The course covers model checking and its role in program verification, verification frameworks for communication protocols, distributed and timed systems, hardware and concurrent programs, the classical modeling approaches, such as timed automata, push-down automata and Petri nets, and the verification of concurrent programs running on weakly consistent platforms such as x86-TSO, ARM, C11 and cloud systems.
The course suits PhD and MSc students with knowledge corresponding to three years of an undergraduate program in computer science. No prior experience of formal methods or weak memory models is assumed.
Lecture recordings
Slides
- Introduction PDF Keynote
- Petri Nets PDF Keynote
- Well-Quasi-Orderings PDF Keynote Summary (Keynote)
- Lossy Channel Systems PDF Keynote
- x86-TSO PDF Keynote Short version (Keynote)
- TSO: The Load-Buffer Semantics PDF Keynote
- Timed Petri Nets PDF Keynote Part 1 (PDF) Part 2 (PDF) Summary (Keynote)
- Stateless Model Checking: The C11 Release-Acquire Semantics PDF Keynote Short version (Keynote)
- View Abstraction PDF Keynote