BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:06e67982-e262-47ae-a23d-86efe1bd8978
X-WR-CALNAME:[MTV] Raphaël Monat - 'Static Type and Value Analysis by Abstr
 act Interpretation of Python Programs with Native C Libraries'
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20231029T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20211031T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20221030T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20210328T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20220327T020000
RDATE:20230326T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:06e67982-e262-47ae-a23d-86efe1bd8978
DTSTAMP:20260418T184108Z
CLASS:PUBLIC
DESCRIPTION:We aim at designing both theoretically and experimentally metho
 ds for the automatic detection of potential bugs in software – or the proo
 f of the absence thereof. This detection is done statically by analyzing p
 rograms' source code without running them. We rely on the abstract interpr
 etation framework to derive sound\, computable semantics. In particular\, 
 we focus on analyzing dynamic programming languages. The target of this wo
 rk is the analysis of Python programs combined with native C libraries.\n
 \n    The abstract interpretation workflow requires a concrete semantics\,
  which will be approximated to create sound computable analyses. Our first
  step is thus to define the uncomputable\, collecting semantics of Python 
 formally. This semantics relies on previous work and retro-engineering fro
 m the source code of the reference interpreter. We took special care to ma
 ke the semantics explainable by providing references to the actual impleme
 ntation's source code for each case of the semantics.\n\n    We have imple
 mented all the analyses presented in this thesis within the Mopsa framewor
 k. From a static analysis developer's perspective\, Mopsa has a double goa
 l. It aims at reducing the cost of lifting an abstract domain from a toy l
 anguage to a real-world one. It also aspires to define relational analyses
  composed of loosely coupled abstract domains that can cooperate. We take 
 particular care to define all our abstract domains independently from each
  other. Mopsa's core is language agnostic\, making Mopsa suitable to analy
 ze different programming languages. The analyses rely on some general use 
 domains\, such as numerical domains\, the recency abstraction of dynamic m
 emory allocation\, and the loop iterator.\n\n    We present a first analys
 is aiming at detecting type-related errors in Python programs. It does so 
 by inferring both the nominal and structural types of objects. Python's ty
 pe annotations can be reused to support libraries. This analysis is refine
 d into a value analysis which is more precise and infers numerical invaria
 nts for the manipulated builtin numeric values. These analyses rely on abs
 tractions of dynamic memory allocation and data structures that we have ad
 apted to the case of dynamic programming languages. Both analyses scale to
  real-world benchmarks a few thousand lines long used by Python developers
 .\n\n    Most Python programs rely on libraries written in C for the sake 
 of performance or code reuse. We define a multilanguage analysis that can 
 detect runtime errors in every part of a multilanguage program: in the Pyt
 hon part\, in the C part\, and at the boundary between the languages. Befo
 re defining this analysis\, we provide an overview of the different intero
 perability mechanisms available between Python and C\, and we define a col
 lecting semantics for the interoperability mechanism provided by the refer
 ence interpreter. This analysis can tackle tests of popular\, real-world l
 ibraries a few thousand lines of C and Python long in a few minutes.
DTSTART;TZID=Europe/Paris:20220216T100000
DTEND;TZID=Europe/Paris:20220216T110000
LOCATION:Zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] Raphaël Monat - 'Static Type and Value Analysis by Abstract I
 nterpretation of Python Programs with Native C Libraries'
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
