UE Analysis and verification of sequential programs

User information

Please note that you are curently looking at the ongoing Academic Programs. Applications are now closed for this academic year (2020-2021) for licences, professional licences, masters, DUT and regulated health training. If you are interested for an application in 2021-2022, please click on this link for the appropriate Academic Programs.

Degrees incorporating this pedagocial element :


The objective of this course is to expose students to the major issues and solutions for the validation of sequential programs. The focus is on the formalization of expected properties and on their verification by deductive and algorithmic methods.

Semantics and logics: Introduction to first-order and higher-order logic, Introduction to the semantics of programming languages (denotational, operational), Formalization of desirable properties (absence of runtime errors, safety violations, termination, examples of security vulnerabilities)

Proof methods: SAT and SMT-solving, Reasoning by induction, Abstract interpretation

Practical static analysis: From C / Java / etc. to formal, Handling pointers, arrays, etc.