Descriptif
This course briefly explores theoretical foundations and practical tools for software verification, with a focus on abstract interpretation based static analysis. Using an abstraction of the program semantics allows us to automatically synthesize inductive program properties. Verification of safety-critical embedded programs is a natural field of application of such techniques. A difficulty that arises is the necessity to take into account the interaction of the program with its physical environment. The system of interest is then hybrid, coupling discrete and continuous components. The second part of the course is devoted to an introduction to the modeling and analysis of such systems.
Topics:
- Inductive Program Verification (4 lectures)
- Semantic equations, fixpoint computation
- Abstract interpretation
- Numerical abstract domains and applications
- Introduction to hybrid systems verification (3 lectures)
Course evaluation:
The course wlll be evaluated on assignments (lab sessions and short exercices directly related to the lecture)
and a project (2nd part of the course, evaluated by report/code + oral defense).
Diplôme(s) concerné(s)
Parcours de rattachement
Format des notes
Numérique sur 20Littérale/grade réduitPour les étudiants du diplôme Conception, Modélisation et Architecture des Systèmes Industriels Complexes
Le rattrapage est autorisé- Crédits ECTS acquis : 2.5 ECTS
La note obtenue rentre dans le calcul de votre GPA.
Pour les étudiants du diplôme Echanges PEI
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 2.5 ECTS
La note obtenue rentre dans le calcul de votre GPA.