Ces analyses couvrent exhaustivement tous les chemins d'exécution et donnent des résultats précis et rapides pour les composants numériques et certains codes de librairie. Dans cet exposé, nous présenterons deux techniques récentes qui permettent d'améliorer les temps d'analyse tout en conservant la finesse de ces diagnostics formels, même en présence de tests instables.

La première technique complémente l'interprétation abstraite de Fluctuat par une compilation abstraite réalisée en deux temps: un plugin de Frama-C transforme le code d'origine en lui rajoutant des points de synchronisations. La librairie float_diagnosis permet ensuite d'instrumenter le code "à la CADNA" de manière à obtenir le diagnostic de précision en exécutant le code instrumenté. Cette technique, couplée avec des scénarios d'analyse fins, permet d'améliorer les temps d'analyse de Fluctuat d'un facteur conséquent sur les codes numériques de plusieurs milliers de lignes de code.

La seconde technique est basée sur des techniques d'accélérations spécifiques aux zonotopes pour améliorer l'atteinte d'un point fixe dans les analyses par interprétation abstraite. Elle synthétise des invariants linéaires inductifs en utilisant une méthode de variation des constantes. Elle se révèle être complète sur la famille des filtres linéaires convergents. Sur la plupart des filtres linéaires testés, elle fournit un invariant en quelques dizaines de cycles d'apprentissage avant de fournir un invariant linéaire 1-inductif. Ce résultat est à comparer avec les résultats de Fluctuat qui requièrent plusieurs milliers cycles pour fournir un invariant k-inductif éventuellement moins précis avec k souvent supérieur à plusieurs centaines.