 | Study programme 2020-2021 | 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 |
| Organisational online arrangements for the end of Q3 2020-2021 assessments (Covid-19) |
|---|
|
| Description of the modifications to the Q3 2020-2021 assessment procedures (Covid-19) |
| As planned. |
Organisational arrangements for the end of Q1 2020-2021 assessments (Covid-19) online or face-to-face (according to assessment schedule)
- Oral exam (questions and answers, presentation of individual or group work, comment and argument about a written text...)
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)