Study programme 20202021  Français  
Project in formal methods for system design (List A)  
Programme component of Master's in Mathematics à la Faculty of Science 
Students are asked to consult the ECTS course descriptions for each learning activity (AA) to know what special Covid19 assessment methods are possibly planned for the end of Q3 

Code  Type  Head of UE  Department’s contact details  Teacher(s) 

USM1SCMATH048M  Optional UE  RANDOUR Mickaël  S820  Mathématiques effectives 

Language of instruction  Language of assessment  HT(*)  HTPE(*)  HTPS(*)  HR(*)  HD(*)  Credits  Weighting  Term 

 Français  40  15  65  0  0  12  12.00  Année 
AA Code  Teaching Activity (AA)  HT(*)  HTPE(*)  HTPS(*)  HR(*)  HD(*)  Term  Weighting 

SMATH043  Formal methods: Introduction  10  0  0  0  0  Q1  
SMATH051  Formal methods: foundations  30  15  5  0  0  Q1  
SMATH056  Formal Methods: Applications  0  0  60  0  0  Q2 
Programme component 

Objectives of Programme's Learning Outcomes
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.
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. 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 of Assessment for UE in Q1
Q1 UE Assessment Comments
Oral exam on theory and exercises (Evaluation E1). Tool presentation by students (Evaluation E2).
Type of Assessment for UE in Q2
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%).
Type of Assessment for UE in Q3
Q3 UE Assessment Comments
Same rules as for Q1/Q2. Any evaluation below 10 must be passed in Q3.
Type of Resit Assessment for UE in Q1 (BAB1)
Q1 UE Resit Assessment Comments (BAB1)
Not applicable.
Type of Teaching Activity/Activities
AA  Type of Teaching Activity/Activities 

SMATH043 

SMATH051 

SMATH056 

Mode of delivery
AA  Mode of delivery 

SMATH043 

SMATH051 

SMATH056 

Required Reading
AA  

SMATH043  
SMATH051  
SMATH056 
Required Learning Resources/Tools
AA  Required Learning Resources/Tools 

SMATH043  Lecture notes available on Moodle. 
SMATH051  Lecture notes available on Moodle. 
SMATH056  Lecture notes available on Moodle. 
Recommended Reading
AA  

SMATH043  
SMATH051  
SMATH056 
Recommended Learning Resources/Tools
AA  Recommended Learning Resources/Tools 

SMATH043  Not applicable 
SMATH051  Not applicable 
SMATH056  Not applicable 
Other Recommended Reading
AA  Other Recommended Reading 

SMATH043  C. Baier, J.P. Katoen. Principles of Model Checking. MIT Press, 2008. 
SMATH051  C. Baier, J.P. Katoen. Principles of Model Checking. MIT Press, 2008. 
SMATH056  C. Baier, J.P. Katoen. Principles of Model Checking. MIT Press, 2008. 