UE Verification of sequential programs

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

Descriptif

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 - Domaine universitaire
Langue(s) : Anglais