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.
None.
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
Evaluation:
- Lab. reports (30 % of the final grade),
- Final Exam (70 % of the final grade)
