Tout développement logiciel est confronté au défi d'éviter les bugs ou, après coup, de vérifier leur absence. L’objectif de cette U.E. est de présenter différentes techniques permettant de garantir la correction d'un logiciel avec un bon degré de confiance. On présentera des méthodes d'analyse statique avec preuves formelles et des méthodes de test.

Première partie : Méthodologie du test de logiciels. Classification des méthodes et types de tests. Tests en boîte blanche/boîte noire. Tests combinatoires, approche pair-wise. Tests aux limites. Critères de couverture et approche par mutations. Tests unitaires et bouchons. Génération automatique de tests par exécution symbolique/concolique.Les liens avec la preuve seront mis en évidence. En TP, mise en oeuvre de test unitaire et logiciel de calcul de couverture.

Deuxième partie : Programmation par contrats. Notion d’invariant de boucle. Logique de Hoare. Calcul de la plus faible précondition. Génération d’obligations de preuves. En TP, mise en oeuvre en langage c à l’aide du langage de spécifications ACSL et du logiciel Frama-c.

À l'issue de cette UE, un étudiant est capable de :
- Mettre en oeuvre des tests unitaires avec calcul de couverture,
- Choisir la méthode de certification/test adaptée aux besoins du projet,
- Écrire une spécification formelle,
- Prouver un programme simple.

- J.-F. Monin, Undestanding Formal Methods, Springer, 2003
- Y. Bertot and P. Casteran, Theorem Proving and Program Development - Coq'Art, Texts in TCS, An EATCS Series, Springer-Verlag, 2004
- J.-R. Abrial, The B_Book - Assigning Programs to Meanings, Cambridge Univ. Press, 1996
- J.-Y. Girard et al., Proofs and Types, In Cambridge Tracts in TCS, Cambridge Univ. Press, 1989
- E. Gamma et al., Design Patterns, Thomson Publishing, 1996

À l'entrée de cette UE, un étudiant devrait avoir suivi ou être capable de :
- Traduire un énoncé de la langue naturelle vers la logique,
- Manipuler un système formel,
- Programmation orientée objet.