FormalMethods-Formal specification and verification of systems


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

Teaching and Learning Methods: Lectures and Lab sessions.

Course Policies: Attendance to the Lab session is mandatory.


There is no textbook for the course. Recommended book for the lab sessions:

  • Book: ABRIAL J-R. The B-book: assigning programs to meanings. Cambridge University Press, 2005, 816p.




Modeling 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 express properties of systems.
  • Be able to reason about systems and to realise the demonstration of properties.
  • Be able to use tools which integrate and automate the formal analysis.

Nb hours: 21.00, at least 3 Lab sessions


  • Lab. reports (30 % of the final grade),
  • Final Exam (70 % of the final grade)