1. Les limites des tests et le mur de l’indécidabilité : pourquoi 1 000 000 de tests réussis ne prouvent rien

1.1 L’aphorisme immortel de Dijkstra et l’explosion combinatoire

En 1969, lors de la conférence de l’OTAN sur le génie logiciel, le lauréat du prix Turing Edsger W. Dijkstra énonça la vérité la plus fondamentale de l’histoire de l’informatique :

“Program testing can be used to show the presence of bugs, but never to show their absence!" (Les tests de programmes peuvent servir à montrer la présence de bugs, mais jamais leur absence !)

Prenons une simple fonction pure f(x, y) acceptant deux entiers signés de 64 bits (int64_t). Le nombre total de paires d’entrées possibles est :

Même avec un supercalculateur testant un milliard ($10^9$) de cas par seconde, il faudrait environ $1,08 \times 10^{22}$ années — soit 780 milliards de fois l’âge de l’univers — pour épuiser toutes les entrées de cette unique fonction ! En présence d’allocations dynamiques sur le tas, de paquets réseau et d’entrelacements (interleavings) non déterministes de threads, le nombre de chemins d’exécution diverge vers l’infini ($\infty$).

En 2006, Joshua Bloch (Google) révéla un bug resté caché pendant 9 ans dans la bibliothèque standard Java (java.util.Arrays.binarySearch) : le célèbre bug de dépassement d’entier de la recherche dichotomique :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

public static int binarySearch(int[] a, int key) {
    int low = 0;
    int high = a.length - 1;
    while (low <= high) {
        int mid = (low + high) / 2; // ★ BUG FATAL : dépassement d'entier si low + high >= 2^31 !
        int midVal = a[mid];
        if (midVal < key) low = mid + 1;
        else if (midVal > key) high = mid - 1;
        else return mid;
    }
    return -(low + 1);
}

Lorsque la somme low + high dépasse $2^{31} - 1 = 2\,147\,483\,647$, l’addition déborde en un nombre négatif en complément à deux, provoquant immédiatement une exception ArrayIndexOutOfBoundsException.

1.2 Le problème de l’arrêt de Turing (1936) et le théorème de Rice (1953)

Pourquoi ne pas construire un analyseur universel capable de décider automatiquement si n’importe quel programme $P$ contient un bug ? Le problème de l’arrêt d’Alan Turing (1936) et le théorème de Rice (1953) prouvent que c’est mathématiquement impossible :

Aucun outil ne peut garantir simultanément : (1) l’automatisation totale, (2) la correction / sûreté (Soundness : zéro faux négatif) et (3) la complétude (Completeness : zéro faux positif).

1.3 Comment la vérification formelle contourne le théorème de Rice : la sur-approximation saine

La vérification formelle refuse tout compromis sur la sûreté (Soundness) : si l’outil certifie le programme "SAFE", il est mathématiquement garanti sans bug sur la totalité de ses $\infty$ exécutions. Pour contourner le théorème de Rice, elle calcule une sur-approximation saine (Sound Over-Approximation) $\mathcal{R}_{\text{approx}} \supseteq \mathcal{R}_{\text{exact}}$ des états accessibles et démontre que son intersection avec les états d’erreur $\mathcal{B}$ est vide :

  flowchart TD
    A["États accessibles exacts R_exact du programme P (Indécidable selon Rice)"] --> B["Les 4 Piliers de la Vérification Formelle"]
    B --> C["Pilier 1 : Vérification Déductive (Logique de Hoare & SMT)"]
    B --> D["Pilier 2 : Model Checking (Logique Temporelle & TLA+)"]
    B --> E["Pilier 3 : Interprétation Abstraite (Connexions de Galois & Astrée)"]
    B --> F["Pilier 4 : Assistants de Preuve (Coq / Rocq, Lean 4, Isabelle)"]
    C --> C1["Invariants de boucle I + preuve automatique des VCs par le solveur SMT Z3"]
    D --> D1["Structure de Kripke M ; exploration symbolique d'états via BDDs/SAT/IC3"]
    E --> E1["Sur-approximation automatique R_exact ⊆ γ(a#) prouvant γ(a#) ∩ Bad = ∅"]
    F --> F1["Isomorphisme de Curry-Howard : termes de preuve vérifiés par un micro-noyau"]

2. Pilier 1 : Vérification déductive — Logique de Floyd-Hoare, plus faible précondition et solveurs SMT

2.1 Le triplet de Hoare, les invariants de boucle et les variants

En 1969, C. A. R. Hoare fonda la logique de Floyd-Hoare autour du triplet de Hoare :

• Correction partielle : Si la précondition $P$ est vraie avant l’exécution de la commande $C$, et si $C$ termine, alors la postcondition $Q$ est vraie après.
• Correction totale : Sous la précondition $P$, $C$ termine obligatoirement en un nombre fini d’étapes et satisfait $Q$.

Les règles d’inférence fondamentales incluent l’axiome d’affectation $\{\,Q[E/x]\,\}\; x := E \;\{\,Q\,\}$ et la règle de la boucle while munie d’un invariant de boucle $I$ et d’un variant (fonction de rang) $V \in \mathbb{N}$ strictement décroissant :

Grâce au calcul de la plus faible précondition (Weakest Precondition, $\text{wp}(C, Q)$) introduit par Dijkstra en 1975, la preuve d’un programme est réduite à des formules logiques appelées conditions de vérification (VCs) : $P \implies \text{wp}(C, Q)$.

2.2 Preuve formelle de la recherche dichotomique avec Dafny et le solveur SMT Z3

En remplaçant le calcul du milieu par mid := low + (high - low) / 2 dans Dafny, Frama-C ou SPARK Ada, le solveur SMT Z3 (architecture DPLL(T) combinant fonctions non interprétées EUF, arithmétique linéaire entière LIA, vecteurs de bits $\mathcal{T}_{\text{BV}}$ et tableaux $\mathcal{T}_{\text{A}}$) démontre automatiquement l’absence totale de dépassement et la correction fonctionnelle :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19

method BinarySearch(a: array<int>, key: int) returns (index: int)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures 0 <= index ==> index < a.Length && a[index] == key
  ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
  var low := 0;
  var high := a.Length;
  while low < high
    invariant 0 <= low <= high <= a.Length
    invariant forall i :: 0 <= i < a.Length && !(low <= i < high) ==> a[i] != key
    decreases high - low
  {
    var mid := low + (high - low) / 2; // Z3 prouve : aucun dépassement et 0 <= mid < a.Length !
    if a[mid] < key { low := mid + 1; }
    else if key < a[mid] { high := mid; }
    else { return mid; }
  }
  return -1;
}

3. Pilier 2 : Model Checking et logique temporelle — Exploration exhaustive des systèmes distribués

3.1 Structures de Kripke et logiques temporelles LTL / CTL

En 1981, Edmund M. Clarke, E. Allen Emerson et Joseph Sifakis (prix Turing 2007) inventèrent le Model Checking, tandis que Leslie Lamport (prix Turing 2013) créa TLA+. Le système concurrent est modélisé par une structure de Kripke $M = (S, S_0, R, L)$, et ses propriétés temporelles sont exprimées en LTL ou CTL :

1. Sûreté (Safety — « Rien de mauvais n’arrive jamais ») : Exclusion mutuelle : $$\text{LTL} : \quad \mathbf{G}\, \neg (\text{crit}_1 \land \text{crit}_2) \qquad \text{CTL} : \quad \mathbf{AG}\, \neg (\text{crit}_1 \land \text{crit}_2)$$
2. Vivacité (Liveness — « Quelque chose de bon finit toujours par arriver ») : Absence de famine : $$\text{LTL} : \quad \mathbf{G}\, (\text{req}_1 \implies \mathbf{F}\, \text{crit}_1) \qquad \text{CTL} : \quad \mathbf{AG}\, (\text{req}_1 \implies \mathbf{AF}\, \text{crit}_1)$$

3.2 Automates de Büchi, BDDs, IC3 et le succès de TLA+ chez AWS

Le Model Checker traduit la négation de la propriété $\neg \varphi$ en un automate de Büchi $A_{\neg \varphi}$ et vérifie que le produit synchrone est vide ($\mathcal{L}(M \times A_{\neg \varphi}) = \emptyset$). Pour vaincre l’explosion combinatoire des états, le Model Checking symbolique utilise les diagrammes de décision binaire (BDDs, Bryant 1986 / McMillan 1990) capables de traiter $10^{20}$ états, ainsi que le Bounded Model Checking (BMC) et IC3 / PDR.

Chez Amazon Web Services (AWS), l’utilisation de TLA+ (TLC) sur S3 et DynamoDB a permis de découvrir, avant même d’écrire le code de production, un bug critique de perte de données nécessitant une séquence précise de 35 étapes entrelacées (partitions réseau, retards de messages, basculement de leader).

4. Pilier 3 : Interprétation abstraite et la catastrophe du vol 501 d’Ariane 5

4.1 4 juin 1996 : Pourquoi la fusée Ariane 5 (370 millions $) a explosé après 37 secondes de vol

Le 4 juin 1996, le vol inaugural (Vol 501) du lanceur européen Ariane 5 s’autodétruisit 37 secondes après le décollage à Kourou, entraînant une perte de 370 millions de dollars. La cause résidait dans le système de référence inertielle (SRI), qui réutilisait un module Ada d’Ariane 4 convertissant une variable flottante 64 bits de vitesse horizontale (BH) en un entier signé 16 bits ($-32\,768 \dots +32\,767$). Plus rapide qu’Ariane 4, Ariane 5 fit dépasser $32\,767$ à BH, déclenchant une exception matérielle de dépassement d’entier (Operand Error) non interceptée. Les deux calculateurs SRI (nominal et secours) s’arrêtèrent et envoyèrent sur le bus une trame de diagnostic binaire que le calculateur de bord (OBC) prit pour une donnée d’attitude réelle, braquant les tuyères au maximum jusqu’à la dislocation du lanceur.

4.2 L’interprétation abstraite de Patrick et Radhia Cousot (1977) et l’analyseur Astrée sur l’Airbus A380

Inventée dès 1977 par les chercheurs français Patrick Cousot et Radhia Cousot, l’interprétation abstraite relie le treillis concret $(\mathcal{C}, \subseteq) = (\mathcal{P}(\Sigma), \subseteq)$ à un treillis abstrait $(\mathcal{A}, \sqsubseteq^\#)$ (intervalles $[a,b]$, octogones $\pm x \pm y \le c$ d’Antoine Miné, polyèdres convexes) par une connexion de Galois :

Grâce à la condition de sûreté locale $\alpha(F(\gamma(a^\#))) \sqsubseteq^\# F^\#(a^\#)$ et à l’opérateur d’élargissement (Widening $\nabla$) qui accélère la convergence des boucles, le point fixe abstrait sur-approxime de façon 100 % fiable tous les états accessibles :

  flowchart TD
    subgraph Concrete["Domaine Concret C = P(Σ) (Infini / Indécidable)"]
        S["Ensemble d'états concrets S"] -->|"Transition concrète F"| FS["États suivants F(S)"]
        LFP_C["États accessibles exacts R_exact = lfp F"]
    end
    subgraph Abstract["Domaine Abstrait A (Intervalles / Octogones / Ellipsoïdes)"]
        A_elem["État abstrait a#"] -->|"Transition abstraite F#"| FA["État abstrait suivant F#(a#)"]
        LFP_A["Point fixe abstrait lfp F# (Convergence par élargissement ∇)"]
    end
    S -->|"Abstraction α(S)"| A_elem
    FA -->|"Concrétisation γ(F#(a#)) ⊇ F(S)"| FS
    LFP_A -->|"Garantie mathématique : R_exact ⊆ γ(lfp F#)"| LFP_C

Développé à l’ENS Paris par l’équipe de Cousot, l’analyseur statique Astrée (combinant intervalles, octogones et domaines ellipsoïdaux pour les filtres numériques du second ordre) a vérifié le logiciel de commandes de vol électriques (Fly-by-Wire) de l’Airbus A380 (près d’un million de lignes de C) avec zéro fausse alarme, prouvant l’absence absolue de toute erreur d’exécution !

5. Pilier 4 : Assistants de preuve (Coq / Rocq, Lean 4, Isabelle) et synthèse comparative

Fondés sur l’isomorphisme de Curry-Howard (une proposition est un type, une preuve est un programme), les assistants de preuve (Coq / Rocq, Lean 4, Isabelle/HOL) ont donné naissance à deux monuments :

1. CompCert (Xavier Leroy, INRIA) : Compilateur C optimisant intégralement prouvé en Coq. Lors des tests par fuzzing Csmith (PLDI 2011), plus de 325 bugs de génération de code ont été trouvés dans GCC et LLVM, mais zéro dans la partie vérifiée de CompCert !
2. seL4 (Gerwin Klein et al.) : Premier micro-noyau de système d’exploitation formellement vérifié en Isabelle/HOL jusqu’au binaire ARM/RISC-V.