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 :
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.
Courses offered by :
In brief
Period : Semestre 9Credits : 6
Number of hours
- Lectures (CM) : 12h
- Practical work (TP) : 12h
- Tutorials (TD) : 12h
Location(s) : Grenoble
Language(s) : English
Contact(s)
David Monniaux
