 | |
| INFO0060-1 | Concurrent System Verification and Temporal Logic
 |
|
| Duration : | 30h Th, 30h Pr |
|
| Credits/ECTS : |
|
|
| Holder(s) : | Bernard Boigelot, Pascal Gribomont, Pierre Wolper |
|
| Language : | Langue française |
|
| 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. |
|
| Course objective : | To introduce the theoretical and algorithmicc foundations of the verification of concurrent systems. |
|
| Prerequisites : | Knowledge of concurrent programming; knowledge of formal logic (course INFO0051-0). |
|
| Workshops : | Use of verification systems. |
|
| Organization : | Lectures, exercises on the lecture material, verification exercises. |
|
| Written notes : | Available on the course web page. |
|
| Assessment : | Oral exam. |
|
| Contacts : | Teachers :
P. Gribomont - Tél. 04/366 26 67 - e-mail gribomont@montefiore.ulg.ac.be
P. Wolper - Tél. 04/366 20 99 - e-mail pw@montefiore.ulg.ac.be
Assistant: information not currently available. |
|
| Remarks : | Additional information can be found on the course web page: http://www.montefiore.ulg.ac.be/~pw/cours/verif.html |
|
