Study programme 2020-2021Français
Formal methods for systems design : fundamentals
Programme component of Master's in Computer Science à la Faculty of Science

Students are asked to consult the ECTS course descriptions for each learning activity (AA) to know what special Covid-19 assessment methods are possibly planned for the end of Q3

CodeTypeHead of UE Department’s
contact details
US-M1-INFO60-027-MOptional UERANDOUR MickaëlS820 - Mathématiques effectives
  • RANDOUR Mickaël

of instruction
of assessment
HT(*) HTPE(*) HTPS(*) HR(*) HD(*) CreditsWeighting Term
  • Français
Français401550066.001st term

AA CodeTeaching Activity (AA) HT(*) HTPE(*) HTPS(*) HR(*) HD(*) Term Weighting
S-MATH-043Formal methods: Introduction100000Q1
S-MATH-051Formal methods: foundations3015500Q1
Programme component

Objectives of Programme's Learning Outcomes

  • Have acquired highly specialised and integrated knowledge and broad skills in the various disciplines of computer science, which come after those within the Bachelor's in computer science.
  • Carry out development or innovation projects in IT.
    • Apply, mobilise, articulate and promote the knowledge and skills acquired in order to contribute to the achievement of a development or innovation project.
    • Master the complexity of such work and take into account the objectives and constraints which characterise it.
  • Master communication techniques.
    • Communicate, both orally and in writing, their findings, original proposals, knowledge and underlying principles, in a clear, structured and justified manner.
    • Adapt their communication to a variety of audiences.
    • Where possible, communicate in a foreign language.
  • Develop and integrate a high degree of autonomy.
    • Aquire new knowledge independently.
    • Pursue further training and develop new skills independently.
    • Develop and integrate a high degree of autonomy to evolve in new contexts.
  • Apply scientific methodology.
    • Critically reflect on the impact of IT in general, and on the contribution to projects.
    • Demonstrate thoroughness, independence, creativity, intellectual honesty, and ethical values.

Learning Outcomes of UE

Thorough understanding of the core concepts of formal methods, mastery of the underlying mathematical frameworks, ability to go further for application on real examples.

Content of UE

Theory: Introduction to formal methods, Modeling systems, Linear temporal logic, Computation tree logic, Symbolic model checking, Model checking probabilistic (and quantitative) systems, Synthesis of probabilistic (and quantitative)
systems, Synthesis via game theory. Tool presentations by students.

Prior Experience

Basic notions of algorithmics, programming, complexity, logic.

Type of Assessment for UE in Q1

  • Presentation and/or works
  • Oral examination

Q1 UE Assessment Comments

Oral exam on theory and exercises (Evaluation E1). Tool presentation by students (Evaluation E2). Final grade for UE. If an evaluation is below 8, the final grade is equal to the minimal evaluation. Otherwise, the following weights are
used: E1 (80%), E2 (20%).

Type of Assessment for UE in Q3

  • Presentation and/or works
  • Oral examination

Q3 UE Assessment Comments

Same rules as for Q1. Any evaluation below 10 must be passed in Q3.

Type of Resit Assessment for UE in Q1 (BAB1)

  • N/A

Q1 UE Resit Assessment Comments (BAB1)

Not applicable.

Type of Teaching Activity/Activities

AAType of Teaching Activity/Activities
  • Cours magistraux
  • Cours magistraux
  • Exercices dirigés
  • Utilisation de logiciels
  • Démonstrations
  • Préparations, travaux, recherches d'information

Mode of delivery

AAMode of delivery
  • Face to face
  • Face to face

Required Reading


Required Learning Resources/Tools

AARequired Learning Resources/Tools
S-MATH-043Lecture notes available on Moodle.
S-MATH-051Lecture notes available on Moodle.

Recommended Reading


Recommended Learning Resources/Tools

AARecommended Learning Resources/Tools
S-MATH-043Not applicable
S-MATH-051Not applicable

Other Recommended Reading

AAOther Recommended Reading
S-MATH-043C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
S-MATH-051C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
(*) HT : Hours of theory - HTPE : Hours of in-class exercices - HTPS : hours of practical work - HD : HMiscellaneous time - HR : Hours of remedial classes. - Per. (Period), Y=Year, Q1=1st term et Q2=2nd term
Date de génération : 09/07/2021
20, place du Parc, B7000 Mons - Belgique
Tél: +32 (0)65 373111