Duration
30h Th, 10h Pr, 20h Proj.
Number of credits
| Master of Science (MSc) in Computer Science and Engineering | 5 crédits | |||
| Master of Science (MSc) in Computer Science | 5 crédits |
Lecturer
Coordinator
Language(s) of instruction
English language
Organisation and examination
Teaching in the second semester
Schedule
Units courses prerequisite and corequisite
Prerequisite or corequisite units are presented within each program
Learning unit 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 learning unit
To introduce the theoretical and algorithmicc foundations of the verification of concurrent systems.
Prerequisite knowledge and skills
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, hybrid learning)
Lectures, exercises on the lecture material, verification exercises.
Organisational adjustments related to the current health context
Recommended or required readings
Available on the course web page.
Assessment methods and criteria
Below you will find information on the evaluation methods planned for in-person and remote exams as well as those planned for hybrid sessions. Depending on how the health crisis evolves, the chosen method will be communicated to you no later than one month before the start of the exam session.
Project, oral exam.
Work placement(s)
Organizational remarks
Contacts
Teachers:
Bernard.Boigelot@uliege.be
Pascal.Gribomont@uliege.be