 | Study programme 2024-2025 | 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 | 20 | 18 | 12 | 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)
Location of learning activity
- Université de Mons - Mons
Location of assessment
- Université de Mons - Mons