UE Analysis and verification of sequential programs

Diplômes intégrant cet élément pédagogique :

Descriptif

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.

 

Informations complémentaires

Méthode d'enseignement : En présence
Lieu(x) : Grenoble - Domaine universitaire
Langue(s) : Anglais