v2.11.0 (5648)

PA - C3B - INF657G : Validation inductive de programmes et de systèmes hybrides (ISC621)

Domaine > Informatique.

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:
  1. Inductive Program Verification (4 lectures)
    • Semantic equations, fixpoint computation
    • Abstract interpretation
    • Numerical abstract domains and applications
  2. 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).

Format des notes

Numérique sur 20

Littérale/grade réduit

Pour les étudiants du diplôme Cyber Physical System

Le rattrapage est autorisé (Note de rattrapage conservée)
    L'UE est acquise si note finale transposée >= C
    • 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)
      L'UE est acquise si note finale transposée >= C
      • Crédits ECTS acquis : 2.5 ECTS

      La note obtenue rentre dans le calcul de votre GPA.

      Veuillez patienter