Duration
20h Th, 20h Pr, 20h Proj.
Number of credits
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. It covers state-space exploration techniques, and their 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 focuses on deductive verification, starting with a brief reminder of propositional satisfiability checking. On this basis, satisfiability modulo theories (SMT) and techniques for combination of theories are introduced. A few major decidable fragments (quantifier-free first-order logic, linear arithmetic on integers and reals) are considered together with suitable decision procedures for usage in SMT solving. Quantifier handling methods in SMT are presented. Finally, some hands-on experience with deductive verification techniques is given using an available SMT based verification platform.
Learning outcomes of the learning unit
Introducing the theoretical and algorithmic foundations of the verification of concurrent systems.
Prerequisite knowledge and skills
Basic knowledge of concurrent programming (INFO9012-1), basic knowledge of formal logic (INFO9015-1).
Planned learning activities and teaching methods
Use of verification systems.
Mode of delivery (face to face, distance learning, hybrid learning)
Face-to-face course
Available on the course web page.
Exam(s) in session
Any session
- In-person
oral exam
Work placement(s)
Organisational remarks and main changes to the course
Contacts
Teachers:
Bernard Boigelot, Pascal Fontaine