UE Analysis and verification of sequential programs

Degrees incorporating this pedagocial element :

Description

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.