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

Formal verification of computer systems

academic year
2023-2024
2024-2025

Course teacher(s)

Jean-François RASKIN (Coordinator)

ECTS credits

5

Language(s) of instruction

english

Course content

Kripke Structures and Labeled Transition Systems, Temporal logics, omega-automata, mu-calculus, Model Checking, Symbolic and efficient Model Checking, Specification Languages and Formal Description Techniques, Testing, Program Verification by Invariant Technique.

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

Oral exam.

Language(s) of evaluation

  • english

Programmes