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: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:20260412T065747Z
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