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/12 12:28] – [Journée APR d'été 2026 à Inria Paris] mineapr:journees:ete2026 [2026/06/22 09:21] (current) – [Programme] mine
Line 3: Line 3:
 le 22 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)
Line 21: Line 22:
     * //Analyse et optimisation de la méthode des ALIAS en arithmétique entière.// Oriane Crouzet (APR,SU)     * //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 78: Line 85:
  
 ---- ----
- 
 **Évaluation automatique de la conformité de simulateurs d’éligibilité aux allocations logement**\\ **Évaluation automatique de la conformité de simulateurs d’éligibilité aux allocations logement**\\
 Matéo Germe (SyCoMoRES, Inria) Matéo Germe (SyCoMoRES, Inria)
Line 88: 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.1781260119.txt.gz · Last modified: by mine