Parosh Aziz Abdulla

Algorithmic Program Verification, Fall 2016.

Postgraduate Course, 10 credits.

News

Next lecture: Friday, 17 February, 10:15-12:00, room 1245.

Background

Current capabilities in computer technology allow enormously complicated implementations of such systems, making the task of producing error-free products more and more difficult. Consequently, it is of great practical and economical importance to develop methods which make the design process less error-prone, and there is a real need of techniques for rigorous verification of software in order to complement testing and guarantee a higher degree of reliability.

Goal

The participants will learn:

  • The principles of model checking, a techniques that has led to the most notable advances in the area of algorithmic program verification during the last 20 years.
  • Frameworks for the verification of communication protocols, distributed systems and algorithms , timed systems, hardware circuits, concurrent programs, and multi-core architectures.
  • Modelling and verification through classical models such as timed automata, push-down automata, Petri nets, and lossy channels systems.
Contents
  • Model checking.
  • Infinite-state models.
  • Reachability analysis.
  • Petri nets.
  • Timed automata.
  • Push-down automata.
  • Lossy channel systems.
  • Well quasi-ordered systems.
  • Program abstraction: monotonic abstraction, view abstraction.
  • Weak memory models.
  • Parameterized systems.
Structure
  • 15 Lectures.
  • Project work. The project will consist of a prototype implementation of some of the algorithms discussed in the class.
Examination
  • Weekly assignments.
  • Project work.
Schedule
  • Registration deadline: 15 September. Send an email with your name to Yunyun Zhu.
  • Start: Friday, 7 October, 10:15-12:00, room 1245.
Prerequisites
  • Course suitable both for PhD and MSc students.
  • Basic knowledge corresponding to three years of an undergraduate program in computer science. However, no deep knowledge of formal methods or program verification is assumed.
Slides
Contact Person