Team APR

User Tools

Site Tools

apr:journees:ete2026

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
apr:journees:ete2026 [2026/06/09 12:23] – mineapr:journees:ete2026 [2026/06/22 09:21] (current) – [Programme] mine
Line 1: Line 1:
 ===== Journée APR d'été 2026 à Inria Paris ===== ===== Journée APR d'été 2026 à Inria Paris =====
  
-le 11 juin 2026+le 22 juin 2026
  
 +co-organisée avec l'équipe Inria Antique
  
 ==== Adresse ==== ==== Adresse ====
Line 11: Line 12:
 75013 Paris\\ 75013 Paris\\
  
-==== Programme (prévisionnel) ====+==== Programme ====
  
   * **09:00-09:30**: café d'accueil   * **09:00-09:30**: café d'accueil
-  * **09:30-11:00**: session d'exposés 1+  * **09:30-10:30**: session d'exposés 1
     * //Formaliser l’exécution de LeanMachines à l’aide du π-calcul.// Danaël Carbonneau (APR, SU)     * //Formaliser l’exécution de LeanMachines à l’aide du π-calcul.// Danaël Carbonneau (APR, SU)
     * //Analyse asymptotique de DOAGs binaires.// Amaury Curiel (APR, SU)     * //Analyse asymptotique de DOAGs binaires.// Amaury Curiel (APR, SU)
-    * //TBA.// Oriane Crouzet (APR,SU) +  * **10:30-11:00**: pause 
-  * **11:00-11:30**: pause +  * **11:00-12:30**: session d'exposés 2 
-  * **11:30-12:30**: session d'exposés 2+    * //Analyse et optimisation de la méthode des ALIAS en arithmétique entière.// Oriane Crouzet (APR,SU)
     * //Repenser la vérification des programmes eBPF : survol des méthodes de vérification statique et dynamique.// Maxime Derri (Whisper, Inria)     * //Repenser la vérification des programmes eBPF : survol des méthodes de vérification statique et dynamique.// Maxime Derri (Whisper, Inria)
-    * //TBA.// Marco Campion (APR, SU)+    * //Partial (in)completeness in program analysis by abstract interpretation.// Marco Campion (APR, SU)
   * **12:30-14:00**: déjeuner (espace au rez de chaussé)   * **12:30-14:00**: déjeuner (espace au rez de chaussé)
   * **14:00-15:30**: session d'exposés 3   * **14:00-15:30**: session d'exposés 3
     * //Évaluation automatique de la conformité de simulateurs d’éligibilité aux allocations logement.// Matéo Germe (SyCoMoRES, Inria)     * //Évaluation automatique de la conformité de simulateurs d’éligibilité aux allocations logement.// Matéo Germe (SyCoMoRES, Inria)
     * //Verifying Rust Programs with Aeneas and Lean.// Aymeric Fromherz (Prosecco, Inria)     * //Verifying Rust Programs with Aeneas and Lean.// Aymeric Fromherz (Prosecco, Inria)
-    * //TBA.//+    * //Termination Resilience Static Analysis.// Caterina Urban (Antique, Inria)
   * **15:30-16:00**: pause   * **15:30-16:00**: pause
   * **16:00-17:15**: discussion sur l'enseignement, bilan APR   * **16:00-17:15**: discussion sur l'enseignement, bilan APR
Line 33: Line 34:
 ---- ----
  
-==== Résumés (à compléter) ====+==== Résumés ====
  
 +**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**\\ **Formaliser l’exécution de LeanMachines à l’aide du π-calcul**\\
 Danaël Carbonneau (APR, SU) Danaël Carbonneau (APR, SU)
Line 40: Line 47:
 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. 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. 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.
  
 ---- ----
Line 64: Line 77:
  
 ---- ----
 +**Verifying Rust Programs with Aeneas and Lean**\\
 +Aymeric Fromherz (Prosecco, Inria)
  
-**Évaluation automatique de la conformité de simulateurs d’éligibilité aux allocations logement +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. 
-après-midi**\\+ 
 +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) Matéo Germe (SyCoMoRES, Inria)
  
Line 75: Line 94:
  
 ---- ----
 +**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).
  
apr/journees/ete2026.1781000588.txt.gz · Last modified: by mine