Differences

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

--- apr:journees:ete2026 [2026/06/12 17:11] – [Programme prévisionnel] mine
+++ apr:journees:ete2026 [2026/06/22 09:21] (current) – [Programme] mine
@@ Line 12: / Line 12: @@
 Paris\\
-==== Programme prévisionnel ====
+==== Programme ====
   * **09:00-09:30**: café d'accueil
@@ Line 27: / Line 27: @@
     * //É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)
-    * //Termination Resilience Static Analysis.// (Antique, Inria)
+    * //Termination Resilience Static Analysis.// Caterina Urban (Antique, Inria)
   * **15:30-16:00**: pause
   * **16:00-17:15**: discussion sur l'enseignement, bilan APR
@@ Line 34: / 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**\\
 Danaël Carbonneau (APR, SU)