apr:journees:ete2025
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
apr:journees:ete2025 [2025/05/14 13:59] mine [Liste préliminaire des intervenants] |
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 | * 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 | * 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 | * **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 | * Mardi 3 juin 2025 | ||
| * **09:00-10:30**: Session exposés 3 | * **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 | * **10:30-11:00**: Pause | ||
| - | * **11:00-12:00**: Session enseignement | + | * **11:00-11:45**: Session enseignement |
| - | * **12:00-13:30**: Déjeuner | + | * **11:45-13:30**: Déjeuner |
| * **13:30-15:00**: Réunion APR | * **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 | * Retour à Paris suggéré par le train de 16:12 au départ de Lille Flandres, arrivée à Paris Nord à 17:18 | ||
| - | ==== Liste préliminaire des intervenants ==== | + | ==== Liste des intervenants ==== |
| * Danaël Carbonneau (APR, SU) | * Danaël Carbonneau (APR, SU) | ||
| * Amaury Curiel (APR, SU) | * Amaury Curiel (APR, SU) | ||
| - | * Julien Forget (CRIStAL, Polytech'Lille) | + | * Julien Forget (SyCoMoRES, Polytech Lille) |
| * Pierre Goutagny (SyCoMoRES, Inria Lille) | * Pierre Goutagny (SyCoMoRES, Inria Lille) | ||
| * Mohamed Kissi (APR, SU) | * Mohamed Kissi (APR, SU) | ||
| Line 66: | Line 75: | ||
| **Polymalys: relational abstract interpretation of assembly code**\\ | **Polymalys: relational abstract interpretation of assembly code**\\ | ||
| - | Julien Forget (CRIStAL, Polytech'Lille) | + | 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. | 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. | ||
| Line 103: | Line 112: | ||
| 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. | 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. | ||
| ---- | ---- | ||
apr/journees/ete2025.1747223997.txt.gz · Last modified: 2025/05/14 13:59 by mine
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Share Alike 4.0 International
