Study programme 2023-2024 | Français | ||
Project in formal methods for system design (List A) | |||
Programme component of Master's in Mathematics (MONS) (day schedule) à la Faculty of Science |
Code | Type | Head of UE | Department’s contact details | Teacher(s) |
---|---|---|---|---|
US-M1-SCMATH-048-M | 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 |
---|---|---|---|---|---|---|---|---|
S-MATH-043 | Formal methods: Introduction | 10 | 0 | 0 | 0 | 0 | Q1 | |
S-MATH-051 | Formal methods: foundations | 30 | 15 | 5 | 0 | 0 | Q1 | |
S-MATH-056 | 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.
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
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)
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
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
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
AA | Type of Teaching Activity/Activities |
---|---|
S-MATH-043 |
|
S-MATH-051 |
|
S-MATH-056 |
|
Mode of delivery
AA | Mode of delivery |
---|---|
S-MATH-043 |
|
S-MATH-051 |
|
S-MATH-056 |
|
Required Learning Resources/Tools
AA | Required Learning Resources/Tools |
---|---|
S-MATH-043 | Lecture notes available on Moodle. |
S-MATH-051 | Lecture notes available on Moodle. |
S-MATH-056 | Lecture notes available on Moodle. |
Recommended Learning Resources/Tools
AA | Recommended Learning Resources/Tools |
---|---|
S-MATH-043 | Not applicable |
S-MATH-051 | Not applicable |
S-MATH-056 | Not applicable |
Other Recommended Reading
AA | Other Recommended Reading |
---|---|
S-MATH-043 | C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. |
S-MATH-051 | C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. |
S-MATH-056 | C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. |