UE Verification of sequential programs

Informations aux utilisateurs

Veuillez noter que vous consultez une page du catalogue de formation 2020-2021. Le recrutement est actuellement terminé pour les licences, licences professionnelles, masters, DUT et formations réglementées de santé. Pour consulter le catalogue des formations 2021-2022, cliquez sur le lien suivant.

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


Program verification consists in proving properties that are true of all executions of the program, regardless of the input. For instance, one may wish to prove that the program may never encounter undefined behaviors or assertion violations, or that its output always satisfies some relationship with its input.

In general, one proves that no program execution encounters some undesirable configuration by exhibiting some property, known as inductive invariant, that holds by induction over the number of steps of the execution and that excludes the undesirable configuration. The difficulty is to find such an inductive invariant. This is the hard problem at the heart of program verification.

Topics discussed in the course include:

  •     Reasoning by induction – Inductive invariants
  •     Abstract interpretation
  •     Program proof methods
  •     Termination arguments
  •     Verification for real languages: C, Java, etc.

Informations complémentaires

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