• Savoir décrire ce qui est attendu d'un programme : spécification.
• Savoir décrire ce que fait réellement un programme : modélisation.
• Savoir vérifier que le programme fait réellement ce qui est attendu : vérification, preuve.

• pour éviter les bugs de conception;
• pour faciliter la maintenance du programme;
• pour servir de base à la documentation du programme;
• pour certifier le programme auprès d'autorités;
• pour servir à la conception de jeux de tests; etc.

• Sécurité ferroviaire/aérienne (absence de collisions);
• Protocoles cryptographiques (sécurité, confidentialité, authentification), commerce électronique;
• Conception de circuits (cf. model-checking);
• OS multi-processeurs (cohérence des caches);
• Bases de données (cohérence des informations);
• Conception de langages de programmation (absence d'erreurs de type à l'exécution);

• Ariane 5 (débordement numérique dans un code inutile; problèmes de deadlocks);
• Thérac 25 (mauvaise gestion d'unités de mesure);
• Bug F00F du Pentium (interférence bus lock/illegal instruction);
• Protocoles de Needham-Schroeder, d'Otway-Rees buggés (cas de figures négligés);

This document was translated from L^AT_EX by H^EV^EA.