Programme
| Heures |
événement |
(+)
|
|
12:30 - 14:00
|
Déjeuner |
|
|
14:00 - 15:30
|
CLAP (Auditorium) |
(+)
|
|
14:00 - 14:30 |
› La recherche en logiciel et le matériel open-source - Christian FABRE, CEA LIST |
|
|
14:30 - 15:00 |
› Quels choix possibles dans les modèles d'exécution bas niveau ? - Henri-Pierre Charles, CEA |
|
|
15:00 - 15:30 |
› Pervasive Portable Performance: quand est-ce qu'on arrive ? - Albert Cohen, Google |
|
|
15:30 - 16:00
|
Pause café |
|
|
16:00 - 17:00
|
HiFi (Auditorium) |
(+)
|
|
16:00 - 16:30 |
› Mixer calculs et interactions sur un FPGA - Loïc Sylvestre, Algorithmes, Programmes et Résolution |
|
|
16:00 - 16:30 |
› Une sémantique de la simulation de systèmes hybrides - Marc Pouzet, École normale supérieure |
|
|
17:00 - 18:00
|
Brain-storming prospective (Auditorium) |
|
| Heures |
événement |
(+)
|
|
09:00 - 10:30
|
CLAP (Auditorium) |
(+)
|
|
09:00 - 09:30 |
› Towards the formalisation of interactive properties - Cécile Marcon, Institut Supérieur de lÁéronautique et de lÉspace |
|
|
09:30 - 10:00 |
› Tracabilité du processus de compilation - Bruno MATEU, IMT Atlantique |
|
|
10:00 - 10:30 |
› SSA Translation Is an Abstract Interpretation - Matthieu Lemerre, CEA LIST |
|
|
10:30 - 11:00
|
Pause café |
|
|
11:00 - 12:30
|
CLAP (Auditorium) - LVP |
(+)
|
|
11:00 - 11:30 |
› Spécification Formelle de Gated-SSA - Delphine Demange, Univ Rennes, Inria, CNRS, IRISA |
|
|
11:30 - 12:00 |
› Preuve formelle d'un analyseur flot de données paramétré par un ordre d'itération - Roméo La Spina, Université de Rennes 1, LANGAGE ET GÉNIE LOGICIEL, Institut national de recherche en informatique et en automatique |
|
|
12:00 - 12:30 |
› Propriété du domaine borné pour la logique temporelle linéaire du premier ordre et applications à la vérification de systèmes à états infinis - Quentin PEYRAS, LRE |
|
|
12:30 - 14:00
|
Déjeuner |
|
|
14:00 - 15:30
|
LVP (Auditorium) |
(+)
|
|
14:00 - 14:30 |
› Execution-time opacity problems in (parametric) timed automata - Dylan Marinho, Laboratoire Lorrain de Recherche en Informatique et ses Applications |
|
|
14:30 - 15:00 |
› Formalizing an Efficient Runtime Assertion Checker for an Arithmetic Language with Functions and Predicates - Thibaut Benjamin, Laboratoire Sûreté des Logiciels |
|
|
15:00 - 15:30 |
› CAISAR: Caractérisation et vérification des propriétés de confiance d'IA - Michele Alberti, Laboratoire Sûreté des Logiciels |
|
|
14:00 - 15:30
|
CLAP (IMAG Salle séminaire 2) |
(+)
|
|
14:00 - 14:30 |
› MLIR - Mehdi Amini, LLVM/MLIR |
|
|
14:30 - 15:00 |
› Optimisation d'opérations tensorielles sparse par compaction des nonzeros sur CPU - Valentin Trophime, Inria - Guillaume Iooss, Inria |
|
|
15:00 - 15:30 |
› OpenXLA: a Modular Open-Source Compiler for ML workload - Mehdi Amini, LLVM/MLIR |
|
|
15:30 - 16:00
|
Pause café (Auditorium) |
|
|
16:00 - 17:00
|
HiFi (Auditorium) |
(+)
|
|
16:00 - 16:30 |
› An Iterative Formal Model-Driven Approach to Railway Systems Validation - Asfand Yar, Laboratoire d'Informatique de Grenoble |
|
|
16:30 - 17:00 |
› Correlating Test Events With Monitoring Logs For Test Log Reduction And Anomaly Prediction - Bahareh Afshinpour, Université Grenoble Alpes |
|
|
17:00 - 18:00
|
Brain-storming prospective (Auditorium) |
|
| Heures |
événement |
(+)
|
|
09:00 - 10:30
|
LVP (Auditorium) |
(+)
|
|
09:00 - 09:30 |
› Enseignement de la vérification de systèmes réactifs paramétrés - Alain Giorgetti, Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) |
|
|
09:30 - 10:00 |
› Définition d'un langage de description d'interface graphique formel - Nicolas Nalpon, epita |
|
|
10:00 - 10:30 |
› Une sémantique des structures, unions et termes indéfinis pour la spécification formelle de C - Louis Gauthier, Laboratoire Sûreté des Logiciels |
|
|
10:30 - 11:00
|
Pause café |
|
|
11:00 - 12:30
|
LVP (Auditorium) - CLAP |
(+)
|
|
11:00 - 11:30 |
› Formally verified block optimizations by symbolic execution modulo invariants - Léo Gourdin, VERIMAG |
|
|
11:30 - 12:00 |
› Interactive Source-to-source Code Optimization with OptiTrust - Thomas Koehler, Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie |
|
|
12:00 - 12:30 |
› An AST for Representing Programs with Invariants and Proofs - Guillaume Bertholon, ICube, Inria Strasbourg - Arthur Charguéraud, ICube, Inria Strasbourg |
|
|
12:30 - 14:00
|
Déjeuner |
|
|
