< Retour au sommaire

Synthèse d'invariant pour bibliothèques de calcul: Retour d'expérience sur l'analyse de filtres linéaires

Franck Védrine le

Lieu: Amphi 33/34

Résumé

Dans ce talk, je présenterai un analyse utilisée pour générer des invariants de boucle, pour des boucles non bornées. C’est une première étape pour la synthèse d’annotations de type ACSL qui seraient pertinentes pour des bibliothèques de calcul. Ce besoin d’annotations formelles est sous-jacent à plusieurs problématiques: comment juger de la pertinence de tel algorithme par rapport à tel autre ? Calcule-t-il plus précisément ? Est-il correctement implémenté sur toute la plage de valeur des utilisations et comment détecter une incohérence ? La documentation est-elle à jour ?

Cette analyse a été instantiée avec succès pour l’analyse de filtres linéaires convergents avec 4 modules – simplification, perturbation, élimination des quantificateurs et résolution de contraintes –. Je détaillerai sur un exemple de filtre l’utilisation de ces modules avant d’expliciter comment ces travaux peuvent être généralisés et coopérer de manière plus large avec des analyses formelles “à la Frama-C” sur des librairies comme “opencv” ou “eigen”. En cas de succès, le challenge suivant consistera à suivre la montée en niveau d’abstraction de ce type de code en s’aidant des premières annotations fournies par le Natural Language Processing de la documentation. Ces travaux ont en partie été réalisés dans le cadre du projet H2020 Decoder

English Version

Invariant Synthesis for Numerical Libraries: Application on Convergent Linear Filters

Abstract

In this talk, I present a code analysis that synthesizes loop invariants for unbounded loops. This is a first step towards the synthesis of meaningful formal annotations for numerical libraries. The need for formal annotations underlies several legitimate questions about a code: how assess the relevance of an algorithm over another one? Does it compute more accurately? Is this correct for the whole range of uses? How is an inconsistency in the algorithm detected? Is the documentation up to date?

This analysis has been successfully instantiated for the analysis of linear convergent filters with 4 modules – simplification, perturbation, quantifier elimination and constraint solving–. I first detail the use of these modules on an example of second order linear filter. Then, I explain how this work is generalized to cooperate with formal analyzes “à la Frama-C” on numerical libraries like “opencv” or “eigen”. If successfull, the next challenge will be the synthesis of provable formal annotations that appear with the abstraction levels of such code: in such a situation we expect to obtain initial partial annotations from a Natural Language Processing of the documentation. Part of this work has been conducted through the H2020 Decoder project.