 | Study programme 2021-2022 | Français | |
| Formal methods: foundations | |||
Learning Activity |
| Code | Lecturer(s) | Associate Lecturer(s) | Subsitute Lecturer(s) et other(s) | Establishment |
|---|---|---|---|---|
| S-MATH-051 |
|
|
| Language of instruction | Language of assessment | HT(*) | HTPE(*) | HTPS(*) | HR(*) | HD(*) | Term |
|---|---|---|---|---|---|---|---|
| Français | Français | 30 | 15 | 5 | 0 | 0 | Q1 |
Content of Learning Activity
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.
Required Learning Resources/Tools
Lecture notes available on Moodle.
Recommended Learning Resources/Tools
Not applicable
Other Recommended Reading
C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
Mode of delivery
- Face to face
Type of Teaching Activity/Activities
- Cours magistraux
- Exercices dirigés
- Utilisation de logiciels
- Démonstrations
- Préparations, travaux, recherches d'information
Evaluations
The assessment methods of the Learning Activity (AA) are specified in the course description of the corresponding Educational Component (UE)
(*) 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