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.
This course contributes to the learning outcomes I.1, I.2, II.1, II.2, II.3, III.1, III.2, III.4, IV.4, VI.1, VII.1, VII.2, VII.3, VII.4, VII.5 of the MSc in computer science and engineering.
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)
Face-to-face course
Additional information:
Lectures, exercises on the lecture material, verification exercises.
Recommended or required readings
Available on the course web page.
Assessment methods and criteria
Project, oral exam.
Work placement(s)
Organizational remarks
Contacts
Teacher:
Bernard.Boigelot@uliege.be