Vérification par Analyse Statique

Vérification déductive : Logique de Hoare, calcul de la précondition la plus faible

Vérification de modèles : BDD, SMT

Interprétation abstraite