FormalMethods-Formal specification and verification of systems


The aims of the course are to provide students with tools that can help to design error-free software/hardware systems. The course  gives both the theoretical foundations and the pratical use of formal methods.

Teaching and Learning Methods : Lectures and Lab sessions.

Course Policies : Attendance to Lab session is mandatory.


Bibliography :  There is no textbook for the course.

Recommended book for the lab sessions:

                «The B-book : assigning programs to meanings»

                Abrial, Jean-Raymond ; Hoare, A ; Chapron, Pierre


There are no prerequisites. This class is open to all students.


Modelling and formally analyzing systems:  Students will learn the fundamentals of classical logic, deductive reasoning, theorem proving,  automata theory, temporal logic and model checking. Practical application of formal methods : Students will learn how to use these methods, and apply them to build reliable systems in various domains.

Learning outcomes:

-      be able to write unambiguous specifications, and to express properties of systems.

-      be able to reason about systems, and to  realise demonstration of properties.

-      be able to use tools which integrate and automate the formal analysis.

Nb hours: 21.00, at least 3 Lab sessions

Grading Policy: Lab reports (30%), Final Exam (70%)