Team APR

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
===== Journée APR d'été 2023 à l'EPITA =====

le 23/06/2023

==== Adresse ====

Amphi 1\\
Rez-de-chaussé\\
Bâtiment Voltaire\\
EPITA\\
14-16 Rue Voltaire\\
94270 Le Kremlin-Bicêtre\\


==== Programme ====

  * **09:30-09:45**: Accueil
  * **09:45-10:45**: Session tutoriel
    * //Programmation à types dépendants avec Lean4.// Frédéric Peschanski (APR, SU)
  * **10:45-11:15**: Pause
  * **11:15-12:45**: Exposés
    * //Une machine abstraite pour l'implémentation générique d'analyses de resource automatisées.// Hector Suzanne (APR, SU)
    * //Verifying a compiler for a synchronous dataflow language with state machines in Coq.// Basile Pesin (PARKAS, Inria)
    * //Principal Geodesic Analysis of Merge Trees and Persistence Diagrams.// Mathieu Pont (APR, SU)
  * **12:45-14:00**: Repas sur la terrasse (3ème étage)
  * **14:00-15:30**: Exposés
    * //Détection de contraintes de cardinalités.// Marie Pelleau (Université Côte d’Azur)
    * //L'utilisation d'ACD dans la bibliothèque Spot.// Alexandre Duretz-Lutz (EPITA)
    * //Génération de générateur pour types contraints.// Ghiles Ziat (EPITA)
  * **15:30-16:00**: Pause
  * **16:00-17:00**: Discussion APR

----


==== Résumés ====

**Programmation à types dépendants avec Lean4**\\
Frédéric Peschanski (APR, Sorbonne Université)\\

D'après le site web de Lean4 - https://leanprover.github.io :
> Lean est un langage de programmation fonctionnelle qui simplifie
> la rédaction de programmes correctes et faciles à maintenir.
> On peut également utiliser Lean4 comme un assistant de preuve.

Ma présentation comportera principalement deux parties :
Tout d'abord, je présenterai (assez superficiellement) les principes
fondamentaux du langage, notamment le lambda-calcul à types dépendants
et les types et familles inductives implémentées en Lean4.
Dans la seconde partie, je présenterai des exemples de programmes
qui mettent en pratique les types dépendants.


----

**Verifying a compiler for a synchronous dataflow language with state machines in Coq**\\
Basile Pesin (PARKAS, Inria Paris)


The Vélus project is a formalization of a synchronous block-diagram language, based on elements from Lustre and Scade 6, in the Coq interactive theorem prover.
It includes a relational formalization of the dataflow semantics of the language, a compiler that uses the CompCert C compiler as a backend to produce assembly code, and an end-to-end proof that the dataflow semantics of the source program is preserved by the trace-based semantics of the generated assembly.
Our recent work extends Vélus with higher-level constructs that are useful to define modal behaviors: switched blocks, shared variables (eg last x), reset blocks, and state machines.

This talk will present this work, including the novel semantic model we developed to integrate these block-based constructions into the existing stream-based model.
We will also show how we compile these constructs.
We will outline the adaptations that must be done to the standard source-to-source rewriting schemes, and the invariants necessary to prove them correct in the context of an interactive theorem prover.
Finally, we will explain how the backend of the compiler also needs to be adapted for efficient compilation of these constructs.

----

**Principal Geodesic Analysis of Merge Trees (and Persistence Diagrams)**\\
Mathieu Pont (APR, SU)

This paper presents a computational framework for the Principal Geodesic Analysis of merge trees (MT-PGA), a novel adaptation of the celebrated Principal Component Analysis (PCA) framework [87] to the Wasserstein metric space of merge trees [92]. We formulate MT-PGA computation as a constrained optimization problem, aiming at adjusting a basis of orthogonal geodesic axes, while minimizing a fitting energy. We introduce an efficient, iterative algorithm which exploits shared-memory parallelism, as well as an analytic expression of the fitting energy gradient, to ensure fast iterations. Our approach also trivially extends to extremum persistence diagrams. Extensive experiments on public ensembles demonstrate the efficiency of our approach - with MT-PGA computations in the orders of minutes for the largest examples. We show the utility of our contributions by extending to merge trees two typical PCA applications. First, we apply MT-PGA to data reduction and reliably compress merge trees by concisely representing them by their first coordinates in the MT-PGA basis. Second, we present a dimensionality reduction framework exploiting the first two directions of the MT-PGA basis to generate two-dimensional layouts of the ensemble. We augment these layouts with persistence correlation views, enabling global and local visual inspections of the feature variability in the ensemble. In both applications, quantitative experiments assess the relevance of our framework. Finally, we provide a C++ implementation that can be used to reproduce our results.

----

**Détection de contraintes de cardinalités**\\
Marie Pelleau (Université Côte d’Azur)

Les solveurs SAT sont utilisés avec succès dans de nombreuses applications combinatoires et du monde réel. Il n'est maintenant pas rare de lire qu’une preuve mathématique implique des centaines de gigaoctets de traces de solveur SAT. L'ampleur de la preuve commence à constituer une véritable limite à l'approche globale. Dans cette présentation, nous proposons de rechercher des contraintes de haut niveau dans les preuves UNSAT. Un travail similaire a été proposé il y a quelques années pour les contraintes de cardinalité les plus simples. Nous étendons cette idée à un cas plus général (sans limitation sur les bornes des contraintes de cardinalité) en généralisant l'algorithme de Bron & Kerbosh (pour l’énumération de cliques dans les graphes) aux hypergraphes. 

----

**L'utilisation d'ACD dans la bibliothèque Spot**\\
Alexandre Duretz-Lutz (EPITA)

La décomposition en cycles alternante (ACD) est une structure qui montre
l'imbrication des cycles acceptants et rejetants dans un ω-automate.
Elle permet notamment de transformer un ω-automate avec condition
d'acceptation quelconque en un automate à parité.  Nous discuterons de
son utilisation dans Spot, initialement motivée par la nécessité de
construire des automates à parité pour synthétiser des contrôleurs
réactifs à partir de spécifications LTL.

Cet exposé est une version étendue du papier "Practical applications of
the Alternating Cycle Decomposition" présenté à TACAS'22 en
collaboration avec Antonio Casares, Klara J. Meyer, Florian Renkin, et
Salomon Sickert.

----

**Génération de générateur pour types contraints**\\
Ghiles Ziat (EPITA)

Il est fréquent de manipuler des valeurs numériques avec
des contraintes non explicitées par leurs types. Par exemple, les
intervalles d'entier sont des couples de nombres avec la
contraintes que le premier (la borne inférieure) soit plus petit
que le deuxième (borne supérieure). Un autre exemple est celui
des arbres binaires de recherche ou les clés doivent etre
rencontrées en ordre croissant lors d'un parcours en profondeur
infixe. Nos travaux proposent de générer automatiquement des
tests unitaires - à partir de la définition de ce genre de types
- pour s'assurer que les contraintes associées au type ne sont
pas violées par certaines fonctions. Pour générer ces tests, nous
calculons, à l'aide de programmation par contrainte, une
représentation de l'espace des habitants de ce type et enfin,
nous générons le code du test qui générera aléatoirement et
uniformément des habitants. Notre méthode est implémentée dans un
prototype de pré-processeur pour OCaml appelé Testify.  Pour
étendre notre méthode aux types récursifs, nous mixons de la
génération de structures de données inductive à l'aide de la
méthode de Boltzmann et la génération en domaines finis
uniformément distribué en utilisant des contraintes globales.,
Nous utilisons clp(fd) de SICStus Prolog comme bibliothèque de
contraintes et la bibliothèque Arbogen en tant que générateur
aléatoire de structures arborescentes.



==== Addresse ====

Amphi 1\\
Rez-de-chaussé\\
Bâtiment Voltaire\\
EPITA\\
14-16 Rue Voltaire\\
94270 Le Kremlin-Bicêtre\\


==== Programme ====

  * **09:30-09:45**: Accueil
  * **09:45-10:45**: Session tutoriel
    * //Programmation à types dépendants avec Lean4.// Frédéric Peschanski (APR, SU)
  * **10:45-11:15**: Pause
  * **11:15-12:45**: Exposés
    * //Une machine abstraite pour l'implémentation générique d'analyses de resource automatisées.// Hector Suzanne (APR, SU)
    * //Verifying a compiler for a synchronous dataflow language with state machines in Coq.// Basile Pesin (PARKAS, Inria)
    * //Principal Geodesic Analysis of Merge Trees and Persistence Diagrams.// Mathieu Pont (APR, SU)
  * **12:45-14:00**: Repas sur la terrasse (3ème étage)
  * **14:00-15:30**: Exposés
    * //Détection de contraintes de cardinalités.// Marie Pelleau (Université Côte d’Azur)
    * //L'utilisation d'ACD dans la bibliothèque Spot.// Alexandre Duretz-Lutz (EPITA)
    * //Génération de générateur pour types contraints.// Ghiles Ziat (EPITA)
  * **15:30-16:00**: Pause
  * **16:00-17:00**: Discussion APR

----

==== Résumés ====

**Programmation à types dépendants avec Lean4**\\
Frédéric Peschanski (APR, Sorbonne Université)\\

D'après le site web de Lean4 - https://leanprover.github.io :
> Lean est un langage de programmation fonctionnelle qui simplifie
> la rédaction de programmes correctes et faciles à maintenir.
> On peut également utiliser Lean4 comme un assistant de preuve.

Ma présentation comportera principalement deux parties :
Tout d'abord, je présenterai (assez superficiellement) les principes
fondamentaux du langage, notamment le lambda-calcul à types dépendants
et les types et familles inductives implémentées en Lean4.
Dans la seconde partie, je présenterai des exemples de programmes
qui mettent en pratique les types dépendants.


----

**Verifying a compiler for a synchronous dataflow language with state machines in Coq**\\
Basile Pesin (PARKAS, Inria Paris)


The Vélus project is a formalization of a synchronous block-diagram language, based on elements from Lustre and Scade 6, in the Coq interactive theorem prover.
It includes a relational formalization of the dataflow semantics of the language, a compiler that uses the CompCert C compiler as a backend to produce assembly code, and an end-to-end proof that the dataflow semantics of the source program is preserved by the trace-based semantics of the generated assembly.
Our recent work extends Vélus with higher-level constructs that are useful to define modal behaviors: switched blocks, shared variables (eg last x), reset blocks, and state machines.

This talk will present this work, including the novel semantic model we developed to integrate these block-based constructions into the existing stream-based model.
We will also show how we compile these constructs.
We will outline the adaptations that must be done to the standard source-to-source rewriting schemes, and the invariants necessary to prove them correct in the context of an interactive theorem prover.
Finally, we will explain how the backend of the compiler also needs to be adapted for efficient compilation of these constructs.

----

**Principal Geodesic Analysis of Merge Trees (and Persistence Diagrams)**\\
Mathieu Pont (APR, SU)

This paper presents a computational framework for the Principal Geodesic Analysis of merge trees (MT-PGA), a novel adaptation of the celebrated Principal Component Analysis (PCA) framework [87] to the Wasserstein metric space of merge trees [92]. We formulate MT-PGA computation as a constrained optimization problem, aiming at adjusting a basis of orthogonal geodesic axes, while minimizing a fitting energy. We introduce an efficient, iterative algorithm which exploits shared-memory parallelism, as well as an analytic expression of the fitting energy gradient, to ensure fast iterations. Our approach also trivially extends to extremum persistence diagrams. Extensive experiments on public ensembles demonstrate the efficiency of our approach - with MT-PGA computations in the orders of minutes for the largest examples. We show the utility of our contributions by extending to merge trees two typical PCA applications. First, we apply MT-PGA to data reduction and reliably compress merge trees by concisely representing them by their first coordinates in the MT-PGA basis. Second, we present a dimensionality reduction framework exploiting the first two directions of the MT-PGA basis to generate two-dimensional layouts of the ensemble. We augment these layouts with persistence correlation views, enabling global and local visual inspections of the feature variability in the ensemble. In both applications, quantitative experiments assess the relevance of our framework. Finally, we provide a C++ implementation that can be used to reproduce our results.

----

**Détection de contraintes de cardinalités**\\
Marie Pelleau (Université Côte d’Azur)

Les solveurs SAT sont utilisés avec succès dans de nombreuses applications combinatoires et du monde réel. Il n'est maintenant pas rare de lire qu’une preuve mathématique implique des centaines de gigaoctets de traces de solveur SAT. L'ampleur de la preuve commence à constituer une véritable limite à l'approche globale. Dans cette présentation, nous proposons de rechercher des contraintes de haut niveau dans les preuves UNSAT. Un travail similaire a été proposé il y a quelques années pour les contraintes de cardinalité les plus simples. Nous étendons cette idée à un cas plus général (sans limitation sur les bornes des contraintes de cardinalité) en généralisant l'algorithme de Bron & Kerbosh (pour l’énumération de cliques dans les graphes) aux hypergraphes. 

----

**L'utilisation d'ACD dans la bibliothèque Spot**\\
Alexandre Duretz-Lutz (EPITA)

La décomposition en cycles alternante (ACD) est une structure qui montre
l'imbrication des cycles acceptants et rejetants dans un ω-automate.
Elle permet notamment de transformer un ω-automate avec condition
d'acceptation quelconque en un automate à parité.  Nous discuterons de
son utilisation dans Spot, initialement motivée par la nécessité de
construire des automates à parité pour synthétiser des contrôleurs
réactifs à partir de spécifications LTL.

Cet exposé est une version étendue du papier "Practical applications of
the Alternating Cycle Decomposition" présenté à TACAS'22 en
collaboration avec Antonio Casares, Klara J. Meyer, Florian Renkin, et
Salomon Sickert.

----

**Génération de générateur pour types contraints**\\
Ghiles Ziat (EPITA)

Il est fréquent de manipuler des valeurs numériques avec
des contraintes non explicitées par leurs types. Par exemple, les
intervalles d'entier sont des couples de nombres avec la
contraintes que le premier (la borne inférieure) soit plus petit
que le deuxième (borne supérieure). Un autre exemple est celui
des arbres binaires de recherche ou les clés doivent etre
rencontrées en ordre croissant lors d'un parcours en profondeur
infixe. Nos travaux proposent de générer automatiquement des
tests unitaires - à partir de la définition de ce genre de types
- pour s'assurer que les contraintes associées au type ne sont
pas violées par certaines fonctions. Pour générer ces tests, nous
calculons, à l'aide de programmation par contrainte, une
représentation de l'espace des habitants de ce type et enfin,
nous générons le code du test qui générera aléatoirement et
uniformément des habitants. Notre méthode est implémentée dans un
prototype de pré-processeur pour OCaml appelé Testify.  Pour
étendre notre méthode aux types récursifs, nous mixons de la
génération de structures de données inductive à l'aide de la
méthode de Boltzmann et la génération en domaines finis
uniformément distribué en utilisant des contraintes globales.,
Nous utilisons clp(fd) de SICStus Prolog comme bibliothèque de
contraintes et la bibliothèque Arbogen en tant que générateur
aléatoire de structures arborescentes.
Team APR

User Tools

Site Tools

Page Tools
