Differences

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

--- apr:journees:ete2025 [2025/04/28 14:38]
127.0.0.1 external edit
+++ apr:journees:ete2025 [2025/06/03 23:20] (current)
mine [Liste préliminaire des intervenants]
@@ Line 11: / Line 11: @@
-==== Programme préliminaire ====
+==== Programme ====
   * Lundi 2 juin 2025
-    * Arrivée en train suggérée à XXX
+    * Arrivée de Paris suggérée par le train de 10:15 au départ de Paris Nord, arrivée à Lille Flandres à 11:18
     * **12:00-13:30**: Déjeuner
-    * **14:00-15:30**: Session exposés 1
+    * **14:00-16:00**: Session exposés 1
-    * **15:30-16:00**: Pause
+      * //Polymalys: relational abstract interpretation of assembly code.// Julien Forget (SyCoMoRES, Polytech Lille)
-    * **16:00-17:30**: Session exposés 2
+      * //CUTECat: Concolic Execution for Computational Law.// Pierre Goutagny (SyCoMoRES, Inria Lille)
-    * **19:30**: dîner
+      * //Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis.// Mamy Razafintsialonina (DILS, CEA LIST & APR, SU)
+    * **16:00-16:30**: Pause
+    * **16:30-18:00**: Session exposés 2
+      * //Mopsa at the Software-Verification Competition.// Raphaël Monat (SyCoMoRES, Inria Lille)
+      * //A Practical Solver for Scalar Data Topological Simplification.// Mohamed Kissi (APR, SU)
+      * //Conception de systèmes réactifs et programmation parallèle de haut niveau sur des architectures FPGA.// Loïc Sylvestre (DI, École Normale Supérieure)
+    * **19:30**: dîner à [[https://estaminetlille.fr/nos-estaminets/lestaminet-du-welsh/|L'Estaminet du Welsh]] (45 rue de Gand, 59800 Lille)
   * Mardi 3 juin 2025
     * **09:00-10:30**: Session exposés 3
+      * //Distributed Discrete Morse Sandwich: Efficient Computation of Persistence Diagrams for Massive Scalar Data.// Ève Le Guillou (APR, SU)
+      * //Vers le multi-raffinement en LeanMachines.// Danaël Carbonneau (APR, SU)
+      * //Unranking lexicographique de partitions d’ensembles sous toutes leurs formes.// Amaury Curiel (APR, SU)
     * **10:30-11:00**: Pause
-    * **11:00-12:00**: Session enseignement
+    * **11:00-11:45**: Session enseignement
-    * **12:00-13:30**: Déjeuner au [[https://www.openstreetmap.org/way/1285890069|CROUS]]
+    * **11:45-13:30**: Déjeuner
     * **13:30-15:00**: Réunion APR
-    * Départ suggéré par le train de
+    * Retour à Paris suggéré par le train de 16:12 au départ de Lille Flandres, arrivée à Paris Nord à 17:18
 ==== Liste des intervenants ====
-  * Julien Courtiel (GREYC, Université de Caen)
+  * Danaël Carbonneau (APR, SU)
-  * Amaury Curiel (APR, LIP6, Sorbonne Université)
+  * Amaury Curiel (APR, SU)
-  * Matthieu Dien (GREYC, Université de Caen)
+  * Julien Forget (SyCoMoRES, Polytech Lille)
-  * Jean-Luc Lamotte (GREYC, Université de Caen)
+  * Pierre Goutagny (SyCoMoRES, Inria Lille)
-  * Ève Le Guillou (APR, LIP6, Sorbonne Université)
+  * Mohamed Kissi (APR, SU)
-  * Marco Milanese (APR, LIP6, Sorbonne Université)
+  * Ève Le Guillou (APR, SU)
-  * Mathieu Pont (APR, LIP6, Sorbonne Université)
+  * Raphaël Monat (SyCoMoRES, Inria Lille)
-  * Keanu Sisouk (APR, LIP6, Sorbonne Université)
+  * Mamy Razafintsialonina (DILS, CEA LIST & APR, SU)
-  * Loïc Sylverstre (APR, LIP6, Sorbonne Université)
+  * Loïc Sylvestre (DI, École Normale Supérieure)
-  * Milla Valnet (APR, LIP6, Sorbonne Université)
 ----
@@ Line 46: / Line 53: @@
 ==== Résumés ====
-**Analyse théorique de l'algorithme git bisect**\\
+**Vers le multi-raffinement en LeanMachines**\\
-Julien Courtiel (GREYC, Université de Caen)
+Danaël Carbonneau (APR, SU)
-Dans le royaume des logiciels de gestion de versions, git
+Event B est une méthode formelle basée sur une notion de machine à états, qui permet de modéliser des systèmes qui peuvent être décrits par un état et des transitions discrètes. Il s'agit d'une approche dite de « correction par construction » : on cherche à construire des logiciels, et s'assurer par cette construction de l'absence d'erreurs. Dans ce cadre, la méthode Event B repose sur la notion de raffinement : on décrit une machine à états abstraite correspondant à une spécification du système qu'on cherche à modéliser, puis on précise cette spécification par une machine concrète.
-est sûrement celui qui est assis sur le trône. Ce logiciel libre et
-populaire dispose de nombreuses fonctionnalités très intéressantes
-dont notamment une, peut-être plus méconnue, qui s'appelle git bisect.
-Il s'agit d'un algorithme qui permet de débusquer l'origine d'un bug
-qui s'est introduit dans un projet.
-L'ensemble des historiques d'un projet formant naturellement un graphe
-(plus précisément un DAG), git bisect peut tout simplement se voir
-comme un algorithme de graphes résolvant un problème connu pour être
-NP-complet. Toutefois, il est surprenant de voir qu'aucune étude
-théorique de sa complexité n'a été menée. Paul Dorbec, Romain Lecoq et
-moi-même, tous trois de l'Université de Caen Normandie, proposons de
-rectifier cela et vérifier les bonnes performances théoriques (ou non)
-de git bisect. Il s'agit de travaux en cours.
-Cet exposé présentera ainsi les faiblesses et les forces de git
-bisect. Tout d'abord, nous donnerons la forme des graphes pour
-lesquels la stratégie de git bisect est totalement catastrophique.
-Ensuite, nous montrerons que pour une certaine classe de graphes qui
-est représentative des graphes "issus de la vie réelle", git bisect
-est en fait une bonne approximation de la stratégie optimale. Enfin,
-nous nous interrogerons sur l'existence d'un meilleur algorithme.
+Le but de cet exposé est de présenter **LeanMachines**, une bibliothèque **Lean**, inspirée par les concepts de la méthode Event B. L'utilisation du langage **Lean** permet d'une part d'utiliser des outils de modélisation fonctionnelle (utilisation des environnements de la programmation fonctionnelle typée comme des outils de modélisation), et d'une autre de pouvoir utiliser son puissant système de types pour pouvoir exprimer les spécification du système sous forme de propositions, et les prouver à l'aide de son langage de tactiques. Nous nous intéresserons plus précisément à la notion de raffinement dans **LeanMachines**. Enfin, nous étudierons en quoi leur encodage nous permet d'exprimer une idée, qui n'était pas présente dans Event B, mais qui permet d'intéressantes réutilisations de spécifications : le raffinement multiple.
 ----
+**Unranking lexicographique de partitions d’ensembles sous toutes leurs formes**\\
-**Unranking des ZDD: Le premier algorithme d’unranking efficace basé sur le principe d’inclusion-exclusion**\\
 Amaury Curiel (APR, SU)
-Les ZDD sont une structure de données introduite en 1993 par S.I. Minato dans [1] permettant de représenter des fonctions booléennes de manière compacte grâce à deux règles de compression.
+Lors de cet exposé, nous nous intéresserons à la génération par unranking lexicographique des 20 structures combinatoires décrites par Kenneth P. Bogart comme les 20 objets les plus fondamentaux en combinatoire.
-Dans cet exposé, nous allons présenter les ZDD et les comparer aux ROBDD [2], une autre structure de données permettant de représenter des fonctions booléennes en utilisant un autre jeu de règles de compression, et nous exhiberons une formule de comptage pour ces structures basée sur le principe d’inclusion-exclusion. Le fait que cette formule ne soit pas constructive pose un problème dans la conception d’algorithmes de génération par [[ https://oeis.org/wiki/Ranking_and_unranking_functions| unranking]].
+Nous nous intéresserons à les générer grâce à des algorithmes de type « unranking », méthode de génération déterministe permettant d’obtenir gratuitement la génération aléatoire et exhaustive selon un ordre prédéfini.
-Nous présenterons donc la manière dont nous avons résolu ce problème pour concevoir le premier algorithme d’unranking efficace basé sur le principe d’inclusion-exclusion.
+Dans la littérature, il est possible de trouver des algorithmes d'unranking lexicographique pour 13 d'entre eux.
-[1] S.-i. Minato, “Zero-suppressed BDDs for set manipulation in combinatorial problems,” in Proceedings of the 30th International Design Automation Conference, in DAC '93. Dallas, Texas, USA: Association for Computing Machinery, 1993, pp. 272–277. doi: 10.1145/157485.164890.
-[2] Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers, no. 8, pp. 677–691, 1986, doi: 10.1109/TC.1986.1676819.
+Cependant, il n'existe à notre connaissance aucun algorithme d'unranking lexicographique pour les problèmes liés aux partitions d'ensembles, qui consistent à répartir n objets distincts dans k récipients pouvant être de nature différente (distincts, k variable, séquence, ensembles, etc.).
+Ce travail s'inscrit dans la continuité d'un projet commencé il y a deux ans, dont une partie a été présentée lors de la conférence AofA 2024.
 ----
+**Polymalys: relational abstract interpretation of assembly code**\\
+Julien Forget (SyCoMoRES, Polytech Lille)
-**Modular Counting of Linear Extensions**\\
+Polymalys is a tool for static analysis of assembly code. It discovers linear relations between data locations (i.e. memory locations as well as registers) of the code. The analysis relies on abstract interpretation using a polyhedra-based abstract domain. We have devised two analyses that use the discovered linear relations to compute upper bounds to loop iterations, or to detect stack smashing.
-Matthieu Dien (GREYC, Université de Caen)
-The counting of linear extensions is a prominent problem about partial orders.
-Unfortunately, the problem is computationally hard and in fact, relatively few counting procedures have been proposed in the literature.
-In this talk, we will present a new counting algorithm based on the modular decomposition of posets.
-This algorithm has a better parametrized complexity than the state of the art.
-Moreover, this approach leads us to consider a new parameter of posets (the BIT-width) with two corresponding conjectures.
 ----
-**Fouille de graphes, application à la chémoinformatique**\\
+**CUTECat: Concolic Execution for Computational Law**\\
-Jean-Luc Lamotte (GREYC, Université de Caen)
+Pierre Goutagny (SyCoMoRES, Inria Lille)
-Cet exposé présente les travaux menés au sein du groupe de
+Many legal computations, including the amount of tax owed by a citizen, whether they are eligible to social benefits, or the wages due to civil state servants, are specified by computational laws. Their application, however, is performed by expert computer programs intended to faithfully transcribe the law into computer code. Bugs in these programs can lead to dramatic societal impact, e.g., paying employees incorrect amounts, or not awarding benefits to families in need. To address this issue, we consider concolic unit testing, a combination of concrete execution with SMT-based symbolic execution, and propose CUTECat, a concolic execution tool targeting implementations of computational laws. Such laws typically follow a pattern where a base case is later refined by many exceptions in following law articles, a pattern that can be formally modeled using default logic. We show how to handle default logic inside a concolic execution tool, and implement our approach in the context of Catala, a recent domain-specific language tailored to implement computational laws. We evaluate CUTECat on several programs, including the Catala implementation of the French housing benefits and Section 132 of the US tax code. We show that CUTECat can successfully generate hundreds of thousands of testcases covering all branches of these bodies of law. Through several heuristics, we improve CUTECat’s scalability and usability, making the testcases understandable by lawyers and programmers alike. We believe CUTECat thus paves the way for the use of formal methods during legislative processes.
-chémoinformatique composé d'informaticiens du laboratoire GREYC et de
-chimistes thérapeutiques du laboratoire CERMN. La collaboration se
-concentre sur la conception de méthodes computationnelles pour
-identifier des (sous-)structures chimiques d'intérêt (pour l'activité,
-la toxicité ...) dans les premières étapes de la découverte de
-médicaments. Pour ce faire, nous nous appuyons sur des données de
-bioactivité stockées dans des bases de données chimiques publiques
-telles que ChEMBL ou des données internes (chimiothèque du CERMN).
-Nous disposons d'informations concernant l'affinité des ligands pour
-les cibles (un ligand est une molécule qui se lie à une cible).
-À partir de ces premières informations, nous calculons des
-associations statistiques mettant en évidence les (sous-)structures
-chimiques dont la présence semble influencer l'interaction d'une
-molécule avec la (les) cible(s) d'intérêt.
-Notre travail est centré sur les caractéristiques pharmacophoriques
+----
-des molécules. Ces caractéristiques correspondent à des fonctions
-chimiques importantes dans les interactions entre les ligands et les
-cibles.  Toutes les méthodes sont basées sur une représentation des
-molécules sous la forme de graphes de caractéristiques
-pharmacophoriques et sur de la fouille de données de sous-graphes
-appelés pharmacophores.
+**A Practical Solver for Scalar Data Topological Simplification**\\
+Mohamed Kissi (APR, SU)
-L'exposé présentera l'approche spécifique du groupe de
+Cet article présente une méthode pratique de simplification topologique pour les champs scalaires. L’objectif est de transformer un champ scalaire initial f en un champ simplifié g, en ne conservant que les paires de persistance significatives tout en supprimant le bruit. Contrairement aux approches existantes centrées sur les extrema, notre méthode prend également en charge des paires complexes, notamment les paires de selles en 3D. Notre algorithme repose sur deux accélérations, spécifiquement conçues pour le problème de la simplification topologique, ce qui permet d’obtenir des gains de performance substantiels et rend la méthode applicable à des jeux de données réels. L’efficacité de l’approche est illustrée par des applications telles que l’extraction de structures filamenteuses et la correction de défauts topologiques sur des surfaces. Une implémentation en C++ est fournie afin d’assurer la reproductibilité des résultats
-chémoinformatique et les résultats obtenus.
 ----
-**TTK is Getting MPI-Ready**\\
+**Distributed Discrete Morse Sandwich: Efficient Computation of Persistence Diagrams for Massive Scalar Data**\\
 Ève Le Guillou (APR, SU)
-This system paper documents the technical foundations for the extension of the Topology ToolKit (TTK) to distributed-memory parallelism with the Message Passing Interface (MPI).
+The persistence diagram, which describes the topological features of a dataset, is a key descriptor in Topological Data Analysis. The "Discrete Morse Sandwich" (DMS) method is currently the most efficient algorithm for computing persistence diagrams of 3D scalar fields on a single node, using shared-memory parallelism.
-While several recent papers introduced topology-based approaches for distributed-memory environments, these were reporting experiments obtained with tailored, mono-algorithm implementations.
-In contrast, we describe in this paper a versatile approach (supporting both triangulated domains and regular grids) for the support of topological analysis pipelines, i.e. a sequence of topological algorithms interacting together.
-While developing this extension, we faced several algorithmic and software engineering challenges, which we document in this paper.
-We describe an MPI extension of TTK's data structure for triangulation representation and traversal, a central component to the global performance and generality of TTK's topological implementations.
-We also introduce an intermediate interface between TTK and MPI, both at the global pipeline level, and at the fine-grain algorithmic level.
-We provide a taxonomy for the distributed-memory topological algorithms supported by TTK, depending on their communication needs and provide examples of hybrid MPI+thread parallelizations.
-Performance analyses show that parallel efficiencies range from 20% to 80% (depending on the algorithms), and that the MPI-specific preconditioning introduced by our framework induces a negligible computation time overhead.
-We illustrate the new distributed-memory capabilities of TTK with an example of advanced analysis pipeline, combining multiple algorithms, run on the largest publicly available dataset we have found (120 billion vertices) on a cluster with 64 nodes (for a total of 1536 cores).
-Finally, we provide a roadmap for the completion of TTK's MPI extension, along with generic recommendations for each algorithm communication category.
-[[https://arxiv.org/abs/2310.08339 | [article]]]
+In this work, we extend DMS to distributed-memory parallelism for the efficient and scalable computation of persistence diagrams for massive datasets across multiple compute nodes. On the one hand, we can leverage the embarrassingly parallel procedure of the first and most time-consuming step of DMS (namely the discrete gradient computation). On the other hand, the efficient distributed computations of the subsequent DMS steps are much more challenging. To address this, we have extensively revised the DMS routines by contributing a new self-correcting algorithm, redesigning key data structures and introducing computation tokens to coordinate distributed computations. We have also introduced a dedicated communication thread to overlap communication and computation.
-----
+Detailed performance analyses show the scalability of our hybrid MPI+thread implementation for strong and weak scaling using up to 16 nodes of 32 cores each (512 cores total). Our implementation outperforms Dipha, the only public implementation for distributed persistence diagram computation, with an average speedup of ×8 on 512 cores. We provide a usage example of our algorithm, available at https://github.com/eve-le-guillou/DDMS-example.
-**Under-approximating Abstract Interpretation**\\
-Marco Milanese (APR, SU)
-Static analysis by abstract interpretation has traditionally focused on
+Finally, we show the capabilities of our algorithm by computing the persistence diagram of a 3D scalar field of 6 billion vertices in 174 seconds with 512 cores.
-program verification, that is on checking that programs are free of bugs.
-However, in practice it is not easy to achieve a low rate of false positives,
-and thus verification techniques are difficult to use to catch bugs. In this PhD
-we explore a different and unconventional analysis, based on abstract
-interpretation, allowing to compute under-approximations and thus catching bugs.
-This analysis infers sufficient pre-conditions for program defects, enabling
-developers to detect real bugs and obtain precise information on the conditions
-where they occur. Our work applies this analysis to the C programming languge:
-firstly, by focusing on numeric properties and more recently by adding support
-for the rest of the language (e.g., pointers, memory allocations). Finally,
-we discuss preliminary results of our experiments and future directions
-of work.
 ----
-**Wasserstein Auto-Encoders of Merge Trees (and Persistence Diagrams)**\\
+**Mopsa at the Software-Verification Competition**\\
-Mathieu Pont (APR, SU)
+Raphaël Monat (SyCoMoRES, Inria Lille)
-This paper presents a computational framework for the Wasserstein auto-encoding of merge trees (MT-WAE), a novel extension of the classical auto-encoder neural network architecture to the Wasserstein metric space of merge trees. In contrast to traditional auto-encoders which operate on vectorized data, our formulation explicitly manipulates merge trees on their associated metric space at each layer of the network, resulting in superior accuracy and interpretability. Our novel neural network approach can be interpreted as a non-linear generalization of previous linear attempts [79] at merge tree encoding. It also trivially extends to persistence diagrams. Extensive experiments on public ensembles demonstrate the efficiency of our algorithms, with MT-WAE computations in the orders of minutes on average. We show the utility of our contributions in two applications adapted from previous work on merge tree encoding [79]. First, we apply MT-WAE to merge tree compression, by concisely representing them with their coordinates in the final layer of our auto-encoder. Second, we document an application to dimensionality reduction, by exploiting the latent space of our auto-encoder, for the visual analysis of ensemble data. We illustrate the versatility of our framework by introducing two penalty terms, to help preserve in the latent space both the Wasserstein distances between merge trees, as well as their clusters. In both applications, quantitative experiments assess the relevance of our framework. Finally, we provide a C++ implementation that can be used for reproducibility.
+Mopsa is a multilanguage static analysis platform relying on abstract interpretation. It is able to analyze C, Python, and programs mixing these two languages; we focus on the C analysis here. It provides a novel way to combine abstract domains, in order to offer extensibility and cooperation between them, which is especially beneficial when relational numerical domains are used. We present the results of our 3-year participation to the international Software-Verification Competition, and reflect on future work.
 ----
-**Wasserstein Dictionaries of Persistence Diagrams**\\
+**Conception de systèmes réactifs et programmation parallèle de haut niveau sur des architectures FPGA **\\
-Keanu Sisouk (APR, SU)
+Loïc Sylvestre (DI, École Normale Supérieure)
-We introduce a multi-scale gradient descent approach for the efficient resolution of the corresponding minimization problem, which interleaves the optimization of the barycenter weights with the optimization of the atom diagrams. Our approach leverages the analytic expressions for the gradient of both sub-problems to ensure fast iterations and it additionally exploits shared-memory parallelism. Extensive experiments on public ensembles demonstrate the efficiency of our approach, with Wasserstein dictionary computations in the orders of minutes for the largest examples. We show the utility of our contributions in two applications. First, we apply Wassserstein dictionaries to data reduction and reliably compress persistence diagrams by concisely representing them with their weights in the dictionary. Second, we present a dimensionality reduction framework based on a Wasserstein dictionary defined with a small number of atoms  and encode the dictionary as a low dimensional simplex embedded in a visual space.
+À l’heure où les systèmes embarqués temps réel doivent exécuter toujours plus de calculs en plus d'interagir avec le monde physique, les architectures matérielles à base de FPGA (Field-Programmable Gate Arrays) constituent une cible de choix pour atteindre des facteurs d'accélération importants tout en maintenant des latences faibles.
-----
+Dans ce contexte, l'exposé présentera ECLAT : un langage généraliste (inspiré d’OCaml) avec une sémantique synchrone pour la conception d'applications fiables et efficaces sur des circuits FPGA. ECLAT permet de composer à la fois des comportements réactifs orientés flot de données et des calculs parallèles en mémoire partagée avec de la concurrence déterministe. Le modèle de calcul proposé est suffisamment précis et expressif pour développer des abstractions de programmation de haut niveau (telles que des squelettes algorithmiques et des machines virtuelles) avec des performances en grande partie prédictibles.
-**Programmation FPGA de bas en haut et vice-versa**\\
+Le langage se veut accessible aux programmeuses et programmeurs de logiciel, tout en offrant un contrôle fin sur les détails d'implantation. Il est d'ailleurs utilisé comme langage support dans un cours de compilation.
-Loïc Sylvestre (APR, SU)
-Les circuits reconfigurables FPGA sont classiquement décrits
-dans des langages synchrones flot de données, tels que VHDL.
-Ces langages permettent d'interagir directement avec le monde
-extérieur (capteurs, actionneurs), d'une façon intrinsèquement
-parallèle et déterministe, en se synchronisant sur une horloge
-globale. La programmation de FPGA dans ces langages est toutefois
-difficile, car de très bas niveau.
-Pour y remédier, je montrerai comment encoder des constructions
-de programmation (fonctions, barrières de synchronisation,
-mémoire partagée), dressant ainsi les bases d'un schéma de
-compilation pour un langage généraliste parallèle sur une cible FPGA.
-Ce présente alors un dilemme : comment garder un contrôle fin,
-de bas-niveau, sur le comportement temporel des applications généralistes ?
-C'est un point important pour l'interaction avec le monde
-extérieur, pour prédire les performances et pour offrir à la fois du
-parallélisme de tâches et de la mémoire partagée (en lecture et en écriture)
-de façon sûre.
-La solution que je propose consiste à donner, à un langage généraliste,
-une sémantique synchrone guidée par la cible FPGA. Il s'agit alors
-de définir un nouveau schéma de compilation pour que l'horloge du modèle
-synchrone du langage corresponde à l'horloge globale de la cible FPGA.
-Le modèle de programmation résultant semble bien adapté
-pour la conception de systèmes embarqués réactifs,
-la programmation d'applications parallèles avec mémoire partagée,
-et l'implantation matérielle de langages de programmation existants.
 ----
-**Static Value Analysis by Abstract Interpretation for Functional Languages**\\
+**Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis**\\
-Milla Valnet (APR, SU)
+Mamy Razafintsialonina (DILS, CEA LIST & APR, SU)
-To prevent programming errors, static analysers have been developed for many languages; here we will focus on functional languages. Verification tools for these languages exist, such as classical type systems or deductive methods, but automatic reasoning on numerical programs has been little explored. In this presentation, I will present my work on value analysis by abstract interpretation of functional languages, a safe and automatic approach to prevent errors at runtime.
+We present a generic and sound approach to incremental static analysis using abstract interpretation, designed to overcome the time cost that hinder its integration into CI/CD pipelines. Existing incremental methods often lack soundness guarantees or are limited to specific analyses or tools. The presented approach leverages the similarity between different program versions to soundly reuse previously computed analysis results. We propose novel methods for summarizing functions and reusing loop invariants. These techniques are formalized, proved sound, implemented in the Eva abstract interpreter of Frama-C, and evaluated on real-world commits of open-source programs. The evaluation demonstrates that the incremental analysis significantly reduces re-analysis time compared to a full analysis, while maintaining soundness and a high level of precision, making it suitable for integrating sound static analysis into CI/CD processes.
-Our first results, based on relational abstract domains and summaries of recursive fields in algebraic types, allow us to analyse first-order recursive functions manipulating recursive algebraic types, and to infer in an abstract domain their input-output relation. These methods have been successfully implemented on the MOPSA multilanguage analysis platform for the OCaml language.
-Our current research aims to retain this compositionality for the analysis of higher-order functions, in order to obtain a precise input-output relationship from their point of definition. I will present our ideas, currently experimentally evaluated.
-----

Team APR

User Tools

Site Tools

Differences

Page Tools