BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//LORIA - ECPv6.15.20//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:LORIA
X-ORIGINAL-URL:https://www.loria.fr
X-WR-CALDESC:Évènements pour LORIA
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20210328T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20211031T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20220327T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20221030T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20230326T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20231029T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20220908T093000
DTEND;TZID=Europe/Paris:20220908T113000
DTSTAMP:20260429T113637
CREATED:20220902T141352Z
LAST-MODIFIED:20220902T142825Z
UID:16751-1662629400-1662636600@www.loria.fr
SUMMARY:Soutenance de thèse : Pierre Lermusiaux (VeriDis)
DESCRIPTION:Pierre Lermusiaux (VeriDis) soutiendra sa thèse intitulée « Analyse statique de transformations pour l’élimination de motifs« \, effectuée sous la direction de Pierre-Étienne Moreau et Horatiu Cirstea. La soutenance aura lieu le jeudi 8 septembre à 9h30 en salle A008 au Loria. \nRésumé :\n\nLa transformation de programmes est une pratique très courante dans le domaine des sciences informatiques. De la compilation à la génération de test en passant par de nombreuses approches d’analyse de codes et de vérification formelle des programmes\, c’est un procédé qui est à la fois omniprésent et crucial au bon fonctionnement des programmes et systèmes informatiques. Cette thèse propose une étude formelle des procédures de transformation de programmes dans le but d’exprimer et de garantir des propriétés syntaxiques sur le comportement et les résultats d’une telle transformation. \nDans le contexte de la vérification formelle des programmes\, il est en effet souvent nécessaire de pouvoir caractériser la forme des termes obtenus par réduction suivant une telle transformation. En s’inspirant du modèle de passes de compilation\, qui décrivent un séquençage de la compilation d’un programme en étapes de transformation minimales n’affectant qu’un petit nombre des constructions du langage\, on introduit\, dans cette thèse\, un formalisme basé sur les notions de filtrage par motif et de réécriture permettant de décrire certaines propriétés couramment induites par ce type de transformations. \nLe formalisme proposé se repose sur un système d’annotations des symboles de fonction décrivant une spécification du comportement attendu des fonctions associées. On présente alors une méthode d’analyse statique permettant de vérifier que les transformations étudiées\, exprimées par un système de réécriture\, satisfont en effet ces spécifications. \n\n\nMembres du jury :\n\nDirecteur de thèse :\n\n\nPierre-Étienne Moreau\, Université de Lorraine\nHoratiu Cirstea\, Université de Lorraine\n\n\nRapporteurs :\n\n\nOlga Kouchnarenko\, Unversité de Franche-Comté\nThomas Genet\, Université de Rennes\n\n\nExaminateurs :\n\n\n\n\nMaribel Fernandez\, King’s College\nMarc Pantel\, ENSEEIHT
URL:https://www.loria.fr/event/soutenance-de-these-pierre-lermusiaux-veridis/
LOCATION:A008
CATEGORIES:Soutenance
END:VEVENT
END:VCALENDAR