 | | |
| INFO0060-1 | Concurrent System Verification and Temporal Logic
|
|
| Duration : | 30h Th, 30h Pr |
|
| Number of credits : |
|
|
| Lecturer : | Bernard Boigelot, Pascal Gribomont, Pierre Wolper |
|
Language(s) of instruction :
|
| French language |
|
Course contents :
|
| The course includes two parts. The first deals with the algorithmic verification of concurrent systems based on state-space exploration. It covers state-space exploration techniques, optimisation of this exploration and its use for checking temporal logic formulas using "model checking". This topic is dealt with using finite automata on infinite words, to which an introduction is given. Symbolic verification methods and techniques for dealing with infinite-state systems are also presented.
The second part of the course, presents methods based on invariants and inductive assertions. Techniques for constructing and checking the validity of invariants are studied. Special attention is given to tools that automate part of the verification process and to the frequent special case in which the majority of the systems variables are Boolean. |
|
Learning outcomes of the course :
|
| To introduce the theoretical and algorithmicc foundations of the verification of concurrent systems. |
|
Prerequisites and co-requisites/ Recommended optional programme components :
|
| Knowledge of concurrent programming; knowledge of formal logic (course INFO0051-0). |
|
Planned learning activities and teaching methods :
|
| Use of verification systems. |
|
Mode of delivery (face-to-face ; distance-learning) :
|
| Lectures, exercises on the lecture material, verification exercises. |
|
Recommended or required readings :
|
| Available on the course web page. |
|
Assessment methods and criteria :
|
| Oral exam. |
|
Organizational remarks :
|
| Additional information can be found on the course web page: http://www.montefiore.ulg.ac.be/~pw/cours/verif.html |
|
Contacts :
|
| Teachers:
Bernard.Boigelot@ulg.ac.be
Pascal.Gribomont@ulg.ac.be
Pierre.Wolper@ulg.ac.be |
|
