Team APR

les 2 et 3 juin 2025

Batiment ESPRIT
avenue Paul Langevin
Villeneuve-d'Ascq, 59650

• Lundi 2 juin 2025
  • 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-16:00: Session exposés 1
    • Polymalys: relational abstract interpretation of assembly code. Julien Forget (SyCoMoRES, Polytech Lille)
    • CUTECat: Concolic Execution for Computational Law. Pierre Goutagny (SyCoMoRES, Inria Lille)
    • 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 à 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-11:45: Session enseignement
  • 11:45-13:30: Déjeuner
  • 13:30-15:00: Réunion APR
  • Retour à Paris suggéré par le train de 16:12 au départ de Lille Flandres, arrivée à Paris Nord à 17:18

• Danaël Carbonneau (APR, SU)
• Amaury Curiel (APR, SU)
• Julien Forget (SyCoMoRES, Polytech Lille)
• Pierre Goutagny (SyCoMoRES, Inria Lille)
• Mohamed Kissi (APR, SU)
• Ève Le Guillou (APR, SU)
• Raphaël Monat (SyCoMoRES, Inria Lille)
• Mamy Razafintsialonina (DILS, CEA LIST & APR, SU)
• Loïc Sylvestre (DI, École Normale Supérieure)

Vers le multi-raffinement en LeanMachines
Danaël Carbonneau (APR, SU)

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.

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
Amaury Curiel (APR, SU)

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. 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. Dans la littérature, il est possible de trouver des algorithmes d'unranking lexicographique pour 13 d'entre eux.

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)

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.

CUTECat: Concolic Execution for Computational Law
Pierre Goutagny (SyCoMoRES, Inria Lille)

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.

A Practical Solver for Scalar Data Topological Simplification
Mohamed Kissi (APR, SU)

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

Distributed Discrete Morse Sandwich: Efficient Computation of Persistence Diagrams for Massive Scalar Data
Ève Le Guillou (APR, SU)

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.

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.

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.

Mopsa at the Software-Verification Competition
Raphaël Monat (SyCoMoRES, Inria Lille)

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.

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)

À 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.

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.

Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis
Mamy Razafintsialonina (DILS, CEA LIST & APR, SU)

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.