Course syllabus

This is a static page where content will remain mostly constant during the course.

See the News and Course Material page for information that is added as the course progresses.

Contact details

The teaching team of this course consists of:

For advice/guidance/help with lab hand-ins: contact the teaching assistants via email. You can, for example, ask for an in-person help session. Students are strongly encouraged to make us of the teaching assistants.

Student representatives for this course:

  • Artur Freitas
  • Samuel Kyletoft
  • Enayatullah Norozi
  • Hanna Schaff
  • Axel Siwmark

The best way to contact them is via direct message on Slack.

Course purpose

The aim of this course is to teach knowledge and skills in, and judgement about, two important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced in three ways: conceptual, theoretical, and practical, using a particular tool. The course builds on skills in first-order logic and temporal logic, and shows how these formalisms can be applied, and extended, for the verification of software.

Schedule

TimeEdit

Course literature

The course does not have mandatory literature. However, the following literature can support learning:

For the first part we partly use the book Principles of the Spin Model Checker, mostly Chapters 1-5. The book is available as E-book from within the Chalmers network. Some additional material for that book, in particular the examples, can be found online. In particular, you find there a few pages "Supplementary material on version 6 of Spin", which corrects some outdated information from the main book.

Literature suggestions for the second part will be put here in the future.

Course design

Formal Methods is a generic term for system design, analysis, and implementation methods that are described and used with mathematical rigour. The purpose is to construct, with high confidence, systems that behave according to their specification. The course introduces practically and theoretically the two most important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced using a concrete tool.

On the model checking side, we use the model checker SPIN. The advantage of an automated method at the same time places restrictions on the kind of properties that can be verified. The lectures cover the following topics:

  • Theoretical foundations of model checking.
  • Property languages and their usage.
  • Performing automated verification with a software model checking tool.

For the deductive verification side, we look at program logics and tools that mechanise those. We will cover topics such as:

  • Hoare and separation logic (standard techniques for proving programs correct)
  • Finding and reasoning about invariants
  • Techniques for making program verification scale.

In addition to the lectures, the course has 6 exercise sessions, which are highly recommended. The questions and tasks which will be discussed in either exercise session are published beforehand. Students should familiarise themselves with the questions before the exercise session.

The course has two mandatory lab hand-ins, one about model checking, and one about deductive verification. Each submission of a lab is either rejected (meaning you must improve it) or accepted (meaning you have passed the lab). If the first submission is rejected you have approxiamtely one week to resubmit a corrected version. It is a requirement to do the labs in pairs.

Changes made since the last occasion

The most significant changes:

  • The second part (deductive verification) of the course is completely redone.
  • The final exam is a written exam (previously it was an oral exam).

Learning objectives and syllabus

Learning objectives:

On successful completion of the course the student will be able to:

Knowledge and understanding

  • explain the potential and limitations of using logic based verification methods for assessing and improving software correctness
  • identify what can and what cannot be expressed by certain specification/modeling formalisms
  • identify what can and cannot be analyzed with certain logics and proof methods,

Skills and abilities

  • express safety and liveness properties of (concurrent) programs in a formal way
  • describe the basics of verifying safety and liveness properties via model checking
  • successfully employ tools which prove or disprove temporal properties
  • write formal specifications of object-oriented system units, using the concepts of method contracts and class invariants
  • describe how the connection between programs and formal specifications can berepresented in a program logic
  • verify functional properties of simple programs with a verification tool

Judgement and approach

  • judge and communicate the significance of correctness for software development
  • employ abstraction, modelling, and rigorous reasoning when approaching the development of correctly functioning software

 

Links to official documents:

Examination form

There are two forms of examination: lab hand-ins and a written exam. The written exam takes place at the end of the course. The lab-hand ins and the written exam can be passed independently. To pass the whole course, it is necessary to pass both written exam and the labs. In case of pass, the grade is determined by the result in the written exam.