info459 - Spécification et vérification du logiciel

Credits

5

Prerequisites

(Licence mention informatique)

Parcours

• optional for the computer science mention of the master of science

Objectives

Sensibiliser à l'utilisation des méthodes formelles (spécification et vérification de programmes) pour l'amélioration de la qualité du logiciel. Présenter les notions théoriques sous-jacentes et les mettre en pratique principalement en utilisant des outils existants de spécification et vérification pour Java.

Organization

week

1

2

3

4

5

6

7

8

9

10

11

12

13

C (1h30)

×

×

×

×

×

×

×

×

×

×

×

×

TD (1h30)

×

×

×

×

×

×

×

×

×

×

×

×

TP (2h)

×

×

×

×

×

Student personal work

about 50h

Evaluation

• for UE without Labs : sup ( Ex, (2Ex + CC)/3)
• for UE with Labs : (2TP + 3 sup(Ex, (2Ex + CC)/3))/5

Contents

• Programmation avec des invariants : logique de Hoare, mise en pratique de la programmation par contrat en Java (ex : outils liés à JML, Jass), utilisation de génération automatique d'obligation de preuves et d'un assistant de preuve pour les résoudre, raffinements.
• Test : généralités (place dans le cycle de développement, techniques de test), mise en pratique du test unitaire en Java (ex : Junit).
• Vérification automatique : systèmes de transition, logique temporelle, algorithmes de "model-checking", mise en pratique sur des programmes Java.

Instructor(s)

Mirabelle Nebut

fichier source pour édition/modification