BEGIN:VCALENDAR CALSCALE:GREGORIAN VERSION:2.0 X-WR-TIMEZONE:Europe/Paris METHOD:PUBLISH PRODID:-//LIP6//www.lip6.fr//FR X-WR-CALNAME;VALUE=TEXT:Séminaire LIP6 X-LIC-LOCATION:Europe/Paris BEGIN:VTIMEZONE TZID:Europe/Paris BEGIN:DAYLIGHT TZOFFSETFROM:+0100 RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU DTSTART:19810329T020000 TZNAME:GMT+02:00 TZOFFSETTO:+0200 END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0200 RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU DTSTART:19961027T030000 TZNAME:GMT+01:00 TZOFFSETTO:+0100 END:STANDARD END:VTIMEZONE BEGIN:VEVENT SUMMARY:Motion du LIP6 au sujet de la transphobie et autres discrimin ations ORGANIZER;CN=:MAILTO: DESCRIPTION:Réuni en conseil de laboratoire le 19 juin 2025, le LIP6 a voté la motion suivante à l'unanimité moins une abstention ... DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20250630T180000 DURATION:PT2H UID:LIP6/SEM/OL287 LOCATION:Sorbonne Université - Faculté des Sciences et Ingénierie - 75005 Paris GEO:48.846643;2.355248 END:VEVENT BEGIN:VEVENT SUMMARY:Deux prix du meilleur papier étudiant pour Wenzheng Wang ORGANIZER;CN=:MAILTO: DESCRIPTION:Doctorant de l'équipe SYEL, Wenzheng Wang a reçu deux p rix du meilleur papier étudiant pour des articles présentés lors d es conférences IEEE BioSMART et IEEE NEWCAS. DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20250630T000000 DURATION:PT2H UID:LIP6/SEM/OL288 LOCATION:Sorbonne Université - Faculté des Sciences et Ingénierie - 75005 Paris GEO:48.846643;2.355248 END:VEVENT BEGIN:VEVENT SUMMARY:Thi-Mai-Trang Nguyen nommée IEEE Senior Member ORGANIZER;CN=Thi-Mai-Trang Nguyen:MAILTO:Thi-Mai-Trang.Nguyen@lip6.fr DESCRIPTION:Chercheuse associée à notre équipe NPA, Thi-Mai-Trang Nguyen a récemment été élevée au rang de Membre Senior de l'IEEE. DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20250630T000000 DURATION:PT2H UID:LIP6/SEM/OL289 LOCATION:Sorbonne Université - Faculté des Sciences et Ingénierie - 75005 Paris GEO:48.846643;2.355248 END:VEVENT BEGIN:VEVENT SUMMARY:Le LIP6 accueille la « Franco-Moroccan Research Center Summe r School on Sustainable AI for Resource-Constrained Healthcare » ORGANIZER;CN=Fabrice Kordon:MAILTO:fabrice.kordon@lip6.fr DESCRIPTION:The theme for 2025 is Sustainable AI for Resource-Constra ined Healthcare. DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20250707T180000 DURATION:PT2H UID:LIP6/SEM/OL290 LOCATION:Sorbonne Université - Faculté des Sciences et Ingénierie - 75005 Paris GEO:48.846643;2.355248 END:VEVENT BEGIN:VEVENT SUMMARY:Une nouvelle version de msolve disponible ORGANIZER;CN=:MAILTO: DESCRIPTION:Issue des travaux de l'équipe PolSys, la bibliothèque m solve vise à résoudre des systèmes polynomiaux en plusieurs variab les. Elle est maintenant disponible en une nouvelle version 0.9.0. DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20250729T180000 DURATION:PT2H UID:LIP6/SEM/OL293 LOCATION:Sorbonne Université - Faculté des Sciences et Ingénierie - 75005 Paris GEO:48.846643;2.355248 END:VEVENT BEGIN:VEVENT SUMMARY:Le projet IPRS intégré sur Measurement Lab ORGANIZER;CN=:MAILTO: DESCRIPTION:Bonne nouvelle pour la sécurité et la stabilité d'Inte rnet : le projet IPRS porté au sein de l'équipe NPA publie désorma is ses données sur Measurement Lab, la plateforme open source d'éva luation du réseau internet mondial. DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20250729T180000 DURATION:PT2H UID:LIP6/SEM/OL294 LOCATION:Sorbonne Université - Faculté des Sciences et Ingénierie - 75005 Paris GEO:48.846643;2.355248 END:VEVENT BEGIN:VEVENT SUMMARY:Best Paper Award reçu à la Conférence ACL 2025 ORGANIZER;CN=:MAILTO: DESCRIPTION:Membre de l'équipe BD, Alla Boutaleb a remporté le Best Paper Award du workshop "Table Representation Learning" lors de l'AC L 2025, la conférence internationale du traitement de langage. Féli citations ! DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20250801T180000 DURATION:PT2H UID:LIP6/SEM/OL295 LOCATION:Sorbonne Université - Faculté des Sciences et Ingénierie - 75005 Paris GEO:48.846643;2.355248 END:VEVENT BEGIN:VEVENT SUMMARY:Best Paper Award reçu à ICNLSP 2025 ORGANIZER;CN=:MAILTO: DESCRIPTION:Présenté lors de l'ICNLSP 2025 par Evangelia Zve (équi pe SMA), le papier "From Outliers to Topics in Language Models: Antic ipating Trends in News Corpora" a été récompensé par un Best Pape r Award. Félicitations ! DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20250903T180000 DURATION:PT2H UID:LIP6/SEM/OL296 LOCATION:Sorbonne Université - Faculté des Sciences et Ingénierie - 75005 Paris GEO:48.846643;2.355248 END:VEVENT BEGIN:VEVENT SUMMARY:Distinguished Poster Award reçu à ISSAC 2025 ORGANIZER;CN=:MAILTO: DESCRIPTION:Membre de l'équipe PolSys, Sriram Gopalakrishnan a reçu le Distinguished Poster Award d'ISSAC 2025, la conférence internati onale de référence en calcul formel. Félicitations ! DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20250910T000000 DURATION:PT2H UID:LIP6/SEM/OL297 LOCATION:Sorbonne Université - Faculté des Sciences et Ingénierie - 75005 Paris GEO:48.846643;2.355248 END:VEVENT BEGIN:VEVENT SUMMARY:Un nouveau projet P2IA démarre chez l'équipe MOCAH ORGANIZER;CN=:MAILTO: DESCRIPTION:Porté par un consortium de recherche mené par l'entrepr ise Edumalin, le projet vise à développer un système d'aide à l'a pprentissage du français pour les élèves du cycle 3 (CM1/CM2/6ème ). DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20250108T000000 DURATION:PT2H UID:LIP6/SEM/OL300 LOCATION:Sorbonne Université - Faculté des Sciences et Ingénierie - 75005 Paris GEO:48.846643;2.355248 END:VEVENT BEGIN:VEVENT SUMMARY:Séminaire pour les Doctorants du LIP6 - Carrière académique ORGANIZER;CN=Fabrice Kordon:MAILTO:Fabrice.Kordon@lip6.fr ATTENDEE;CN=Fabrice KORDON;CUTYPE=INDIVIDUAL;PARTSTAT=ACCEPTED:mailto :Fabrice.Kordon@lip6.fr DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20260526T140000 DURATION:PT2H URL;VALUE=URI:https://www.lip6.fr/liens/organise-fiche.php?ident=O1224 UID:LIP6/SEM/O1224 LOCATION:Campus Pierre et Marie Curie, salle Jacques Pitrat (25-26/10 5) GEO:48.847047;2.354619 END:VEVENT BEGIN:VEVENT SUMMARY:[Séminaire MoVe] Yann Thierry-Mieg (MoVe, LIP6) : Modélisat ion et vérification de systèmes complexes. ORGANIZER;CN=Dylan Marinho:MAILTO:Dylan.Marinho@lip6.fr ATTENDEE;CN=Yann Thierry-Mieg (MoVe, LIP6);CUTYPE=INDIVIDUAL;PARTSTAT =ACCEPTED:mailto:Dylan.Marinho@lip6.fr DESCRIPTION:Cet exposé présentera les grandes lignes de mon travail , depuis les diagrammes de décisions hiérarchiques à des langages de haut niveau (GAL/ITS) pour la modélisation des systèmes.  L'exp osé sera peu technique; il balaiera quelques résultats anciens (pre 2015) et certains plus récents mélant des surapproximations SMT, d es sous approximations (heuristiques) et des réductions structurelle s. L'ensemble de ces méthodes sert l'objectif d'analyser des systèm es complexes, typiquement concurrents, et de prouver formellement des propriétés sur leurs comportements possibles. DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20260507T140000 DURATION:PT2H URL;VALUE=URI:https://www.lip6.fr/liens/organise-fiche.php?ident=O1230 UID:LIP6/SEM/O1230 LOCATION:Salle 24-25/405, Campus Pierre et Marie Curie GEO:48.847449;2.355255 END:VEVENT BEGIN:VEVENT SUMMARY:[Séminaire MoVe] ORGANIZER;CN=Dylan Marinho:MAILTO:Dylan.Marinho@lip6.fr DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20260522T140000 DURATION:PT2H URL;VALUE=URI:https://www.lip6.fr/liens/organise-fiche.php?ident=O1231 UID:LIP6/SEM/O1231 LOCATION:Salle 24-25/405, Campus Pierre et Marie Curie GEO:48.847449;2.355255 END:VEVENT BEGIN:VEVENT SUMMARY:[Séminaire MoVe] ORGANIZER;CN=Dylan Marinho:MAILTO:Dylan.Marinho@lip6.fr DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20260619T140000 DURATION:PT2H URL;VALUE=URI:https://www.lip6.fr/liens/organise-fiche.php?ident=O1232 UID:LIP6/SEM/O1232 LOCATION:Salle 24-25/405, Campus Pierre et Marie Curie GEO:48.847449;2.355255 END:VEVENT BEGIN:VEVENT SUMMARY:Abstract Interpretation of Temporal Safety Effects of Higher Order Programs ORGANIZER;CN=Antoine Mine:MAILTO:Antoine.Mine@lip6.fr ATTENDEE;CN=Eric Koskinen (Stevens Institute of Technology);CUTYPE=IN DIVIDUAL;PARTSTAT=ACCEPTED:mailto:Antoine.Mine@lip6.fr DESCRIPTION:In recent years temporal verification has been increasing ly applied to higher-order programs. Some researchers have developed automated approaches via higher-order recursion schemes, reductions t o fair-termination or constrained Horn clauses, while others have ext ended type and effect systems to reason about liveness properties. De spite these works, today's automated tools are often limited to somew hat small examples. In this talk I will discuss our recent work on a new abstract interpretation-based approach to verify temporal safet y properties of recursive, higher-order programs. We begin with a new automata-based “abstract effect domain” for summarizing context- sensitive dependent effects, capable of abstracting relations between the program environment and the automaton control state. Our analysi s includes a new transformer for abstracting event prefixes to automa tically computed context-sensitive effect summaries, and is instantia ted in a type-and-effect system grounded in abstract interpretation. Since the analysis is parametric on the automaton, we next instantiat e it to a broader class of history/register (or “accumulator”) au tomata, beyond finite state automata to express some context-free pro perties, input-dependency, event summation, resource usage, cost, equ al event magnitude, etc. We implemented a prototype evDrift that com putes dependent effect summaries (and validates assertions) for OCaml -like recursive higher-order programs. As a basis of comparison, we d escribe reductions to assertion checking for higher-order but effect- free programs, and demonstrate that our approach outperforms prior to ols Drift, RCaml/Spacer, MoCHi, and ReTHFL. Overall, across a set of 23 benchmarks, Drift verified 12 benchmarks, RCaml/Spacer verified 6, MoCHi verified 11, ReTHFL verified 18, and evDrift verified 21; evDr ift also achieved a 6.3x, 5.3x, 16.8x, and 6.4x speedup over Drift, R Caml/Spacer, MoCHi, and ReTHFL, respectively, on those benchmarks tha t both tools could solve. This work appeared in OOPSLA 2025 and is j oint with Mihai Nicola, Chaitanya Agarwal, and Thomas Wies. DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20260519T110000 DURATION:PT2H URL;VALUE=URI:https://www.lip6.fr/liens/organise-fiche.php?ident=O1238 UID:LIP6/SEM/O1238 LOCATION:Salle 428, couloir 26-00, 4 place Jussieu - 75005 Paris GEO:48.84669;2.354759 END:VEVENT BEGIN:VEVENT SUMMARY:Thèse Marco MILANESE : Interprétation abstraite sous-approx imée et inférence de préconditions libérales ORGANIZER;CN=Marco MILANESE:MAILTO:Marco.Milanese@lip6.fr DESCRIPTION:L’analyse statique automatique des logiciels repose tra ditionnellement sur des sur-approximations du comportement des progra mmes afin de garantir qu’aucune trace d'exécution ne contrevient à une propriété spécifiée. Cependant, ces sur-approximations pe uvent entraîner des faux positifs, qui sont particulièrement inacce ptables dans des environnements non critiques. En revanche, les appr oches d’inférence par sous-approximation, bien qu’elles risquent de ne pas trouver toutes les erreurs, apparaissent plus pertinentes lorsque des garanties de correction strictes ne sont pas essentielles , car elles assurent que chaque violation détectée correspond effec tivement à une erreur. Cette thèse présente un cadre d’analyse s tatique en arrière basé sur l’interprétation abstraite, visant à réaliser une sous-approximation du comportement des programmes. Cette méthode calcule des préconditions suffisantes et peut être a ppliquée, par exemple, pour dériver des préconditions libérales e n vue de la détection d’erreurs au moment de l’exécution ou pou r inférer des contrats de code visant à garantir la correction du p rogramme. L’approche est à la fois complète et entièrement autom atisée. Les contributions de ce travail sont doubles. Premièrement , nous étendons le modèle sémantique et les domaines abstraits afi n de permettre l’analyse de langages similaires au C dans des conte xtes réalistes. Cela inclut l’introduction d’opérateurs de sous -approximation pour les domaines abstraits (comme les intervalles, le s polyèdres et les constructions ensemblistes) ainsi que des extensi ons du modèle sémantique pour prendre en compte les débordements d’entiers et les instructions d’entrée. Afin de permettre une un e prise en compte raisonnable de la mémoire, nous étendons à la fo is le langage et son modèle sémantique afin de tenir compte des ac cès mémoire bas-niveau (par exemple via des pointeurs) ainsi que de s allocations et des libérations dynamiques de mémoire. Cette exte nsion est réalisée grâce au développement d’une sémantique con crète en arrière et d’une abstraction fondée sur le domaine des cellules et une abstraction du tas basée sur l'abstraction des alloc ations récentes. Deuxièmement, ces avancées théoriques sont inté grées dans l’outil d’analyse statique MOPSA, où une analyse en arrière par sous-approximation est mise en œuvre pour assurer à la fois des raisonnements numériques et de mémoire. Nous décrivons brièvement les modifications nécessaires dans l’analyseur, telles que les extensions des signatures de domaines et les mises à jour d es mécanismes d’évaluation des expressions, et nous présentons u ne évaluation expérimentale portant sur la précision et la perform ance. L’outil a été testé lors de la compétition de vérificati on logicielle (SV-COMP), où il a montré une bonne précision dans l es catégories MemSafety et NoOverflows, ayant réussi à analyser 45 % des tâches. Cependant, la précision est plus faible dans les ca tégories ReachSafety et SoftwareSystems, en raison de la complexité accrue des propriétés à vérifier et de la taille plus grande des programmes impliqués. Bien que notre analyseur soit en général mo ins précis que les outils de pointe, il nécessite des ressources bi en inférieures : en moyenne, les outils concurrents consomment entre 38% et 220% plus de temps. En résumé, ce travail étend les techni ques d’interprétation abstraite pour l’inférence de pré-condit ions suffisantes, passant d’une base théorique à une méthode pra tique et applicable aux langages de programmation réels. DTSTAMP:20260422T010700Z DTSTART;TZID=Europe/Paris:20260427T140000 DURATION:PT2H URL;VALUE=URI:https://www.lip6.fr/actualite/personnes-fiche.php?ident=D2615 UID:LIP6/SEM/D2615 LOCATION:Campus Pierre et Marie Curie, salle Jacques Pitrat (25-26/10 5) GEO:48.847047;2.354619 END:VEVENT END:VCALENDAR