1. Accueil
  2. EN
  3. Studying at ULB
  4. Find your course
  5. UE
INFO-F412

Formal verification of computer systems

academic year
2024-2025
2025-2026

Course teacher(s)

Jean-François RASKIN (Coordinator)

ECTS credits

5

Language(s) of instruction

english

Course content

  • Introduction: notion of specification and formal verification.
  • Labeled transition systems, automata, and temporal logics (LTL and CTL).
  • Safety and liveness properties.
  • Behavioral equivalence and reductions.
  • Timed automata.
  • Markov chains and Markov decision processes.

Objectives (and/or specific learning outcomes)

Study of the techniques and existing tools to formally specify and verify critical systems.

Prerequisites and Corequisites

Cours ayant celui-ci comme co-requis

Teaching methods and learning activities

Ex-cathedra course and practical works.

References, bibliography, and recommended reading

  • Model Checking - Clarcke, E., O. Grumberg et D. Peled, Mit Press, 1999.

    Principles of Model-Checking. C. Baier and J.P. Katoen. Mit Press, 2006.

Other information

Contacts

Prof. Jean-François Raskin

Email: jraskin [at] ulb.ac.be

Campus

Plaine

Evaluation

Method(s) of evaluation

  • Oral examination
  • Other

Oral examination

Other

Written exam.

Language(s) of evaluation

  • english

Programmes