Study programme 2025-2026Français
Project in formal methods
Programme component of Master's in Teaching (Section 4) : Mathematics (MONS) (day schedule) à l"Teacher Training School

CodeTypeHead of UE Department’s
contact details
Teacher(s)
UF-M1-MEMAT4-015-MOptional UERANDOUR MickaëlS820 - Mathématiques effectives
  • RANDOUR Mickaël

Language
of instruction
Language
of assessment
HT(*) HTPE(*) HTPS(*) HR(*) HD(*) CreditsWeighting Term
  • Français
Français301872001010.00Année

AA CodeTeaching Activity (AA) HT(*) HTPE(*) HTPS(*) HR(*) HD(*) Term Weighting
S-MATH-043Formal methods: Introduction100000Q1
S-MATH-051Formal methods: foundations20181200Q1
S-MATH-056Formal Methods: Applications006000Q2

Overall mark : the assessments of each AA result in an overall mark for the UE.
Programme component

Objectives of Programme's Learning Outcomes

  • Skills for organising and supporting learning in an evolving dynamic.
    • Understand the subject content, its epistemological foundations, its scientific and technological development, its didactics and teaching methodology.

Learning Outcomes of UE

Thorough understanding of the core concepts of formal methods, mastery of the underlying mathematical frameworks, ability to apply them to practical cases using software tools, ability to include formal methods in software development processes, understanding of advanced work in the field.

UE Content: description and pedagogical relevance

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. Presentation of advanced work on verification and synthesis of computer systems. Project: system development using formal methods.

Prior Experience

Basic notions of algorithmics, programming, complexity, logic.

Type(s) and mode(s) of Q1 UE assessment

  • Oral examination - Face-to-face
  • Oral presentation - Face-to-face

Q1 UE Assessment Comments

Oral exam on theory and exercises (Evaluation E1). Tool presentation by students (Evaluation E2).

Method of calculating the overall mark for the Q1 UE assessment

Individual evaluations only. Global grade at Q2.

Type(s) and mode(s) of Q1 UE resit assessment (BAB1)

  • N/A - Néant

Q1 UE Resit Assessment Comments (BAB1)

Not applicable.

Method of calculating the overall mark for the Q1 UE resit assessment

Not applicable.

Type(s) and mode(s) of Q2 UE assessment

  • Production (written work, report, essay, collection, product, etc.) - To be submitted in class
  • Oral examination - Face-to-face
  • Oral presentation - Face-to-face
  • Practical exam - Face-to-face

Q2 UE Assessment Comments

Presentations of advanced work based on scientific articles or books (Evaluation E3). Project (possibly within a group) (Evaluation E4). 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 (40%), E2 (10%), E3 (20%), E4 (30%).

Method of calculating the overall mark for the Q2 UE assessment

Presentations of advanced work based on scientific articles or books (Evaluation E3). Project (possibly within a group) (Evaluation E4). 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 (40%), E2 (10%), E3 (20%), E4 (30%).

Type(s) and mode(s) of Q3 UE assessment

  • Production (written work, report, essay, collection, product, etc.) - To be submitted in class
  • Oral examination - Face-to-face
  • Oral presentation - Face-to-face
  • Practical exam - Face-to-face

Q3 UE Assessment Comments

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

Method of calculating the overall mark for the Q3 UE assessment

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

Type of Teaching Activity/Activities

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

Mode of delivery

AAMode of delivery
S-MATH-043
  • Face-to-face
S-MATH-051
  • Face-to-face
S-MATH-056
  • Face-to-face

Required Learning Resources/Tools

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

Recommended Learning Resources/Tools

AARecommended Learning Resources/Tools
S-MATH-043Not applicable.
S-MATH-051Not applicable.
S-MATH-056Not 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.
S-MATH-056C. 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 dernière mise à jour de la fiche ECTS par l'enseignant : 05/05/2025
Date de dernière génération automatique de la page : 14/03/2026
20, place du Parc, B7000 Mons - Belgique
Tél: +32 (0)65 373111
Courriel: info.mons@umons.ac.be