Presentation of the fundamental principles and formal tools at the basis of all methods of design, verification and implementation of computer systems. Thus, the fundamental notions of mathematical logic and automatic demonstration at the basis of all these techniques of modeling and verification of computer systems are addressed. Classical logic formalisms such as propositional logic and first order logic, but also non-classical logic formalisms such as modal logic (widely used for multi-agent systems and data representation) are presented.
Teaching time performed: 6 hours of lectures, 3 hours of tutorials, and 3 hours of practical classes in Coq.
Part of the teaching team for the school year 2021-2022 and 2022-2023.
Instructors: Marc Aiguier, Pascale Le Gall, and Fabrice Popineau.
Student level: Third year (~M2/MSc).
Syllabus