Introduction and objectives

This course provides an introduction to formal techniques to verify computer systems based on models (model checking).

The official plan of this course is hosted in FCUP here.

Learning outcomes and competences

Students should:

understand the importance of using logic and formal methods in the development of complex computer systems; and
be able to model simple systems and specify properties using temporal logics.

19 Sep ‘24: Overview of the module and introduction to model checking (Slides 1-intro.pdf). Starting to describe transition systems with functors (slides 2-behaviour, frames 1-6).
24 Sep ‘24: Transition systems with functors; syntax of sequential process algebra (slides 2-behaviour, frames 6-18).
26 Sep ‘24: Syntax and semantics of CCS (slides 2-behaviour, frames 18-29).
1 Oct ‘24: Modelling in mCRL2 (slides 3-mCRL2, frames 1-12).
3 Oct ‘24: No lesson.
8 Oct ‘24: Equivalence of transition systems (slides 2-behaviour, frames 13-38).
10 Oct ‘24: Modal logics (slides 4-modal-logic.pdf, frames 1-24).
15 Oct ‘24: Exercises: specifying and explaining concrete formulas in process logic; process logic with regular expressions (slides 4-modal-logic.pdf, frames 25-31).
17 Oct ‘24: Modal logic in mCRL2 (slides 3-mCRL2; Process logic vs. bisimulations (slides 4-modal-logic.pdf, frames 33-…).

Principles of model checking., Christel Baier and Joost-Pieter Katoen; ISBN: 978-0-262-02649-9

- - José Proença
  - - DCC 1.69
    - jose.proenca(at)fc.up.pt
    - meet: thu afternoon (email before)

Edit the content of this page here.