Static Type Analysis by Abstract Interpretation of Python Programs (Artifact)

Authors Raphaël Monat , Abdelraouf Ouadjaout , Antoine Miné

Thumbnail PDF

Artifact Description

  • Filesize: 0.52 MB
  • 6 pages

Document Identifiers

Author Details

Raphaël Monat
  • Sorbonne Université, CNRS, LIP6, Paris, France
Abdelraouf Ouadjaout
  • Sorbonne Université, CNRS, LIP6, Paris, France
Antoine Miné
  • Sorbonne Université, CNRS, LIP6, Paris, France
  • Institut Universitaire de France, Paris, France

Cite AsGet BibTex

Raphaël Monat, Abdelraouf Ouadjaout, and Antoine Miné. Static Type Analysis by Abstract Interpretation of Python Programs (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 11:1-11:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)



Python is an increasingly popular dynamic programming language, particularly used in the scientific community and well-known for its powerful and permissive high-level syntax. Our work aims at detecting statically and automatically type errors. As these type errors are exceptions that can be caught later on, we precisely track all exceptions (raised or caught). We designed a static analysis by abstract interpretation able to infer the possible types of variables, taking into account the full control-flow. It handles both typing paradigms used in Python, nominal and structural, supports Python’s object model, introspection operators allowing dynamic type testing, dynamic attribute addition, as well as exception handling. We present a flow- and context-sensitive analysis with special domains to support containers (such as lists) and infer type equalities (allowing it to express parametric polymorphism). The analysis is soundly derived by abstract interpretation from a concrete semantics of Python developed by Fromherz et al. Our analysis is designed in a modular way as a set of domains abstracting a concrete collecting semantics. It has been implemented into the MOPSA analysis framework, and leverages external type annotations from the Typeshed project to support the vast standard library. We show that it scales to benchmarks a few thousand lines long, and preliminary results show it is able to analyze a small real-life command-line utility called PathPicker. Compared to previous work, it is sound, while it keeps similar efficiency and precision.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
  • Software and its engineering → Semantics
  • Formal Methods
  • Static Analysis
  • Abstract Interpretation
  • Type Analysis
  • Dynamic Programming Language
  • Python Semantics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Davide Ancona, Massimo Ancona, Antonio Cuni, and Nicholas D. Matsakis. Rpython: a step towards reconciling dynamically and statically typed OO languages. In DLS, pages 53-64. ACM, 2007. Google Scholar
  2. Levin Fritz and Jurriaan Hage. Cost versus precision for approximate typing for Python. In PEPM, pages 89-98. ACM, 2017. Google Scholar
  3. Aymeric Fromherz, Abdelraouf Ouadjaout, and Antoine Miné. Static value analysis of Python programs by abstract interpretation. In NFM, volume 10811 of LNCS, pages 185-202. Springer, 2018. Google Scholar
  4. Mostafa Hassan, Caterina Urban, Marco Eilers, and Peter Müller. MaxSMT-based type inference for Python 3. In CAV (2), volume 10982 of LNCS, pages 12-19. Springer, 2018. Google Scholar
  5. M. Journault, A. Miné, R. Monat, and A. Ouadjaout. Combinations of reusable abstract domains for a multilingual static analyzer. In Proc. of the 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE19), pages 1-17, July 2019. Google Scholar
  6. Pytype., 2019. Accessed: 2019-10-22.