le 22 juin 2026
co-organisée avec l'équipe Inria Antique
Auditorium Jacques-Louis Lions
Centre Inria de Paris
48 rue Barrault
75013 Paris
Partial (in)completeness in program analysis by abstract interpretation.
Marco Campion (APR, SU)
Abstract interpretation, introduced by Patrick and Radhia Cousot in 1977, is a unifying framework for reasoning about program behavior by soundly approximating program semantics over an abstract domain. Soundness guarantees that no real behavior is missed, at the price of precision, since the abstraction may introduce spurious behaviors. In static program analysis, these spurious behaviors manifest as false alarms. In practice, the usefulness of such an analysis hinges on how few false alarms it produces, and the natural ideal is completeness: an analysis that raises none at all. This ideal, however, is impossible to achieve in general, and the reason is fundamental: by Rice’s theorem, the exact verification of non-trivial semantic properties is undecidable. The thesis of this talk is that this should not be read as a defeat but as an invitation: rather than asking whether an analysis is complete, we should ask how and to what extent it fails to be. From this perspective, I will introduce the basic principles of abstract interpretation with an emphasis on intuition, recall the notion of completeness, and then present partial completeness as a framework for formally reasoning about controlled, bounded forms of incompleteness in abstract interpretation.
Formaliser l’exécution de LeanMachines à l’aide du π-calcul
Danaël Carbonneau (APR, SU)
LeanMachines est un framework s’inspirant de la méthode Event B afin de spécifier des programmes réactifs dans l’assistant de preuves Lean4. En LeanMachines, il est possible de spécifier des événements, de prouver des propriétés sur ces derniers, mais également de composer ces spécifications. Il n’est cependant pas encore possible de faire de même pour les machines qui exécutent ces événements : le cadre actuel ne formalisant que leurs transitions, et pas leur comportement à l’exécution. Afin de résoudre ce problème, nous proposons d’intégrer des machines, dont les événements ont été spécifiés en LeanMachines, dans des processus de π-calcul. Cette approche permettrait à la fois de spécifier et raisonner sur des réseaux composés de plusieurs machines interagissant entre elles, mais aussi de pouvoir exprimer et vérifier des propriétés sur leur exécution à l’aide de techniques issues du domaine des algèbres de processus.
Analyse et optimisation de la méthode des ALIAS en arithmétique entière.
Oriane Crouzet (APR,SU)
La méthode des ALIAS est un algorithme classique, développé dans les années 1970, permettant de générer en temps constant des variables aléatoires suivant une distribution discrète. Toutefois, cette approche présente certaines limites, notamment le recours à l’arithmétique flottante, susceptible d’introduire des erreurs d’arrondi. Afin d'améliorer la méthode classique des ALIAS, de nouveaux algorithmes ont été développés. Parmi eux, certains visent à approcher au plus près l’optimalité de la méthode de génération aléatoire proposée par Knuth et Yao. L’objectif de cet exposé est d'explorer une nouvelle version de la méthode des ALIAS reposant sur l’arithmétique entière, en la comparant aux approches déjà existantes dans l'état de l'Art. Une attention particulière sera portée à l’optimisation de la consommation de bits aléatoires lors du tirage ainsi qu’à l’évaluation des performances temporelles de ce nouvel algorithme.
Analyse asymptotique de DOAGs binaires
Amaury Curiel (APR, SU)
Les graphes dirigés, acycliques ordonnés (DOAGs) apparaissent naturellement comme structures de données pour représenter des objets partageant des sous-structures communes. Dans cet exposé, nous nous intéressons à deux familles de DOAGs: les variantes unaire-binaire et binaire. Nous cherchons à comprendre combien il en existe lorsque leur taille devient grande, ainsi qu’à comprendre la répartition typique de certains paramètres.
Nous présentons d’abord un résultat de comptage asymptotique : le nombre de DOAGs binaires à 𝑛 nœuds croît comme Θ(𝑛!4𝑛 exp(3𝑎1𝑛^1/3)√𝑛), où 𝑎1 est la plus grande racine de la fonction d’Airy. Ce comportement, dit en exponentielle étirée, est obtenu grâce à une méthode de type “guess and check” que nous détaillerons.
Nous abordons ensuite l’étude de paramètres pour les DOAGs de “petite hauteur droite”. En étendant un cadre combinatoire issu de l’énumération des arbres relaxés, nous obtiendrons des équations fonctionnelles décrivant nos structures que nous étudierons à l’aide de méthodes issues de la combinatoire analytique afin de comprendre la répartition asymptotique de certains paramètres
Repenser la vérification des programmes eBPF : survol des méthodes de vérification statique et dynamique
Maxime Derri (Whisper, Inria)
Extended Berkeley Packet Filter (eBPF) est une technologie permettant d'étendre le noyau d'un système d'exploitation en y chargeant des programmes écrits en espace utilisateur. Intégré au noyau Linux depuis 2014, eBPF a permis l'émergence d'une grande variété de projets dans des domaines tels que l'observabilité, la sécurité, les systèmes ou encore les réseaux. Contrairement aux modules noyau, l'objectif d'eBPF est de proposer une interface stable et de permettre le chargement de programmes dans le noyau par des utilisateurs non privilégiés. Pour garantir la sécurité du système, Linux s'appuie sur un analyseur statique, appelé vérificateur eBPF, chargé de s'assurer que les programmes eBPF respectent un ensemble de contraintes de sécurité.
Cependant, la présence de bugs, de problèmes de soundness ainsi que l'absence de fondations formelles ont rendu cet objectif difficile à atteindre. En conséquence, plusieurs systèmes d'exploitation basés sur le noyau Linux ont introduit des mécanismes visant à réduire les risques associés à eBPF : exigence de privilèges spécifiques pour utiliser le sous-système eBPF, restriction d'une partie de ses fonctionnalités, désactivation de l'appel système bpf, etc. Par ailleurs, l'architecture même du vérificateur eBPF constitue un frein à l'expressivité des programmes. Ces limitations ont favorisé l'émergence d'outils de vérification alternatifs, chacun apportant ses avantages, mais aussi ses inconvénients.
L'objectif de cette présentation est de proposer un survol des deux grandes familles d'outils de vérification de programmes eBPF, en mettant en évidence les avantages et les limites de ces approches. Nous commencerons par une courte introduction de la technologie eBPF. Nous présenterons ensuite des outils d'analyse statique fondés sur l'interprétation abstraite. Enfin, nous nous intéresserons à des méthodes de vérification dynamique par isolation, dans lesquelles les programmes eBPF sont instrumentés et vérifiés pendant leur exécution.
Verifying Rust Programs with Aeneas and Lean
Aymeric Fromherz (Prosecco, Inria)
Aeneas est un outil de vérification de programmes Rust. En se reposant sur le système de borrows et la discipline d'ownership au coeur du langage Rust, Aeneas traduit des programmes Rust safe vers des modèles fonctionnels équivalents dans des assistants de preuves tels que Lean. Cette traduction permet d'éviter de devoir raisonner sur la mémoire des programmes, simplifiant grandement le processus de vérification formelle.
Dans cette présentation, nous présenterons les idées derrière la traduction fonctionnelle d'Aeneas, l'utilisation de Lean, et le développement de tactiques spécifiques à Aeneas, et discuterons des applications récentes à la vérification de primitives cryptographiques post-quantiques.
Évaluation automatique de la conformité de simulateurs d’éligibilité aux allocations logement
Matéo Germe (SyCoMoRES, Inria)
Dans cette présentation, je vais expliquer le travail que j’ai réalisé pour comparer automatiquement les résultats de Catala et d’OpenFisca-France sur le calcul des aides au logement. J’ai mis en place une chaîne de traitement qui permet de lancer des tests, de récupérer les résultats, puis de repérer les écarts entre les deux systèmes. L’objectif est ensuite d’analyser ces différences afin de comprendre d’où elles proviennent. Ce travail permet donc de vérifier la fiabilité des simulateurs utilisés pour estimer les droits aux aides sociales.
Termination Resilience Static Analysis
Caterina Urban (Antique, Inria)
We present a novel abstract interpretation-based static analysis framework for proving Termination Resilience, the absence of Robust Non-Termination vulnerabilities in software systems. Robust Non-Termination characterizes programs where an untrusted (e.g., externally-controlled) input can force infinite execution, independently of other trusted (e.g., internally-controlled) variables. Our framework is a semantic generalization of Cousot and Cousot’s abstract interpretation-based ranking function derivation, and our sound static analysis extends Urban and Miné’s decision tree abstract domain in a non-trivial way to manage the distinction between untrusted and trusted program variables. The talk concludes with open challenges in dealing with angelic non-determinism, pointer-manipulating programs, and going beyond termination to program properties expressed in Computational Tree Logic (CTL) or Alternating-Time Temporal Logic (ATL).