Aller au menu Aller au contenu
Une voie, plusieurs choix
Informatique et Mathématiques appliquées
Une voie, plusieurs choix

> Formation > Cursus ingénieur

Program Testing and Verification - WMM9MO73

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail cet article Facebook Twitter Linked In
  • Number of hours

    • Lectures : 18.0
    • Tutorials : -
    • Laboratory works : -
    • Projects : -
    • Internship : -
    • Written tests : -
    ECTS : 3.0
  • Officials : David MONNIAUX

Goals

Understanding the various approaches used for testing and proving code, their strength and limitations.

Content

Testing is a well-known approach for ascertaining if a program works correctly: one runs the program, or parts thereof, on examples (handwritten or sometimes automatically generated) and checks that the output fits the specification. Even if there is no specification, it is at least implicit that the program should not crash.

Yet testing suffers from a major weakness: it checks a finite number of cases and a bug may be unnoticed if it is not triggered by any of these. Symbolic testing was introduced: through symbolic execution the program is executed with some input values kept symbolic: for instance instead of considering that input variable _x_ is 5 for testing, we will keep it symbolic and thus explore the code for all possible values of _x_. This is much more thorough than normal testing (also known as concrete testing), but also much more difficult to perform: the program may have to be explored through different paths, and sophisticated algorithms are used to check for infeasible paths. Since keeping everything symbolic is complicated and costly, and sometimes impossible (when executing system calls, for instance) most tools do a mixture of concrete and symbolic execution, also known as concolic testing.

In general, symbolic testing cannot prove that a program will not encounter a bug, because of the possibly infinite number of execution steps to simulate. Proving that a program works as intended is actually much like proving mathematical theorems: one proves a property by induction on the number of steps that the program executes (or number of loop iterations, etc.). One important difficulty is that the property that can be proved by induction (known as an inductive invariant) is not necessarily the final property that we are interested in. Providing suitable inductive invariants is human intensive, and thus much work has been put into automating both finding such invariants and then proving that they are inductive.

Results from Turing (and Gödel etc.) show that general automation in program proofs and theorem proving is impossible. This does not prevent partial yet industrially relevant solutions.

Prerequisites

Fluency with programming in general.
C language.
Knowledge of first-order logic and basic mathematics.

Tests

practical assignment (30%) and final exam (70%)

70% final exam
30% practical assignment

The exam is given in english only FR

Calendar

The course exists in the following branches:

  • Curriculum - Master in Computer Science - Semester 9 (this course is given in english only EN)
see the course schedule for 2022-2023

Additional Information

Course ID : WMM9MO73
Course language(s): FR

You can find this course among all other courses.

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail cet article Facebook Twitter Linked In

Date of update September 21, 2022

Université Grenoble Alpes