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%)
