It is virtually impossible to guarantee correctness of a system, and in turn the absence of bugs by standard software engineering practice such as code review, systematic testing and good software design alone. The complexity of systems is typically too high to be manageable by informal reasoning or reasoning that is not tool supported. The formal methods community has developed various rigorous, mathematically sound techniques and tools that allow the automatic analysis of systems and software. The application of these fully automatic techniques is typically called algorithmic verification. The course will describe several automatic verification techniques, the algorithms they are based on, and the tools that support them. We will discuss examples to which the techniques have been applied, and provide experience with the use of several state-of-the-art analysis tools.

Objectives of the Course

The goal is to educate students on the concepts of algorithmic verification and give them hands-on experience in modern verification tools.

Technical aspects covered

The topics covered by the lectures will educate students on the foundations of automata theory and temporal logics, LTL and CTL model checking techniques and model checking tools, the application of static analysis techniques to program verification, and modern advanced verification techniques for timed and probabilistic systems.

During the course, students are exposed to a scientific theory of algorithmic verification techniques, the underlying concepts for state-of-the-art tools, and sound frameworks for program analysis.

Learning Outcomes

After completing this course, students should:

  • Be able to distinguish between the various automatic formal methods available, weighing up their advantages and disadvantages.
  • Be able to develop formal models of software systems, amenable to automatic verification.
  • Be able to specify software using program logics such as temporal logic.
  • Develop a scientific understanding of algorithmic verification techniques, including the underlying concepts for state-of-the-art tools.
  • Understand the role of abstraction in formal methods and its uses to simplify models and make verification feasible.
  • Be able to use various algorithmic verification tools.

Assumed Knowledge

Students need to have understanding of discrete mathematics, and basic knowledge in a programming language such as C.

The course makes use of a number of discrete mathematics concepts. Students may find the course very difficult without MATH1005 or equivalent discrete mathematics background.

Completion, or undertaking of automata and/or logic courses such as COMP1600 or COMP2620 are desirable for getting the most out of the course, but not essential.

Course philosophy and teaching strategies

The learning focus in this course is primarily on lectures and assignments, plus a mid term project which you can use to demonstrate your skills acquired until then. While marks are assigned to the assignments, their primary purpose is to give you concrete tasks with deadlines to help you structure your learning.

Lecturers and Tutors

If you’re stuck, then you can reach out for help anytime—the course help page or course forum is a good place to start.

bars search times arrow-up