Home - Search by Faculty - By teacher - By course


INFO0060-1

Concurrent System Verification and Temporal Logic

[ version française ]

Duration :30h Th, 30h Pr
Credits/ECTS :
4th year of the 5 year degree in civil engineering in electricity (electronics)6,5
5th year of the 5 year degree in civil engineering in electricity (electronics)6,5
4th year of the 5 year degree in civil engineering in computer sciences5,5
2nd "licence" in computer6
Holder(s) :Pascal Gribomont, Pierre Wolper
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 algorithmluc foundations of the verification of concurrent systems.
Prerequisites : Knowledge of concurrent programming (course INFO0012-1) and 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




ULg : Students and Studies Administration - Academic Affairs
Contact : Monique Marcourt, direction A.E.E.
Date of data : 27/02/2006
Developed by SEGI