- 4MMACSCS

Goal(s)

This course is an introduction to formal methods for software analysis
(deductive verification, abstract interpretation, symbolic execution) and their applications for software safety and security, and (middle-end) compiler optimizations.

Responsible(s)

Sylvain BOULME

Content(s)

• Compared Semantics of programming languages (C, Java, Rust, etc).
• Axiomatic semantics and deductive verification (Floyd-Hoare-Dijkstra logic).
• Introduction to Abstract Intepretations and Data-flow Analyses.
• Examples of value analyses, liveness analyses and taint analyses.
• Application to safety of critical systems.
• Application to middle-end compiler optimizations (e.g. constant propagation, dead-code eliminations).
• Software Security : attacks, exploits and hardening
• Tools for pentest.

• knowledge of C and assembly.
• langage theory (contex-free grammars, attribute grammars).
• basic knowledge of calculability theory (halt and Rice theorems).
• basic knowledge in compiler design (parsing, abstract syntax trees, syntax-directed-translation).
• (partial) implementation of a compiler.
• basic knowledge in first order logic (models and inference rules).

Test

Evaluation : Examen écrit (2h)

Resit : Examen écrit (2h)

Written exam 2h.

Calendar

The course exists in the following branches:

• Curriculum - Core curriculum - Semester 8

Additional Information

Course ID : 4MMACSCS
Course language(s):

You can find this course among all other courses.