16 Search Results for "Monat, Raphaël"

Issue

DARTS, Volume 11, Issue 2

Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Editors: Karine Even-Mendoza, Raphaël Monat, and Yannick Zakowski

Issue

DARTS, Volume 10, Issue 2

Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Editors: Karine Even-Mendoza and Raphaël Monat

Document
Artifact
DOI: 10.4230/DARTS.12.1.3
The Virtual Recency Abstraction (Artifact)

Authors: Sven Keidel, Raphaël Monat, and Sebastian Erdweg

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
Abstract interpreters enable sound static analysis, but are hard to develop. In recent years, researchers have proposed a component-based approach to developing abstract interpreters, where different parts of the abstract domain (e.g., numeric, call frame, heap) are handled by isolated components. This works well as long as components do not share or expose their internal state: Any state update that is locally sound is also globally sound. However, some abstract domains require shared state, most prominently relational abstract domains, which use symbolic expressions such as 2x + 5 to represent abstract values. As the relational component performs a strong update of x, the abstract value 2x + 5 can change non-monotonically, which breaks soundness. We propose a novel solution to this problem: A virtual recency abstractions that decouples the relational component, supports strong updates, and allows recursion. We prove that the virtual recency abstraction restores soundness: Any shared state wrapped in our virtual recency abstraction may be locally updated non-monotonically, while global soundness persists. We applied our approach to develop the first relational WebAssembly analysis, reusing many components from an existing inter-procedural abstract interpreter. Furthermore, we evaluate the recall, precision, and scalibility of this analysis to demonstrate the practicality of the virtual recency abstraction.
Cite as

Sven Keidel, Raphaël Monat, and Sebastian Erdweg. The Virtual Recency Abstraction (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{keidel_et_al:DARTS.12.1.3,
  author =	{Keidel, Sven and Monat, Rapha\"{e}l and Erdweg, Sebastian},
  title =	{{The Virtual Recency Abstraction (Artifact)}},
  pages =	{3:1--3:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Keidel, Sven and Monat, Rapha\"{e}l and Erdweg, Sebastian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.3},
  URN =		{urn:nbn:de:0030-drops-261405},
  doi =		{10.4230/DARTS.12.1.3},
  annote =	{Keywords: Relational Numerical Analysis, Recency Abstraction}
}
Document
Artifact
DOI: 10.4230/DARTS.12.1.6
Comparing Transparent Static Analyzers with Open Verification Dashboard (Artifact)

Authors: Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
This artifact accompanies the eponymous article. It enables reproduction of the experimental claims made in the article that are covered by this description.
Cite as

Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat. Comparing Transparent Static Analyzers with Open Verification Dashboard (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{goalard_et_al:DARTS.12.1.6,
  author =	{Goalard, Tom and Holter, Karoliine and Saan, Simmo and Vojdani, Vesal and Monat, Rapha\"{e}l},
  title =	{{Comparing Transparent Static Analyzers with Open Verification Dashboard (Artifact)}},
  pages =	{6:1--6:15},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Goalard, Tom and Holter, Karoliine and Saan, Simmo and Vojdani, Vesal and Monat, Rapha\"{e}l},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.6},
  URN =		{urn:nbn:de:0030-drops-261430},
  doi =		{10.4230/DARTS.12.1.6},
  annote =	{Keywords: automated static analysis, multi-tool integration, interoperability, proof obligations, result aggregation, verification progress, selectivity metric, reproducibility, dashboard}
}
Document
Artifact
DOI: 10.4230/DARTS.12.1.15
DelExp: A Relational Container Abstraction With Applications to Compositional Analysis (Artifact)

Authors: Milla Valnet, Raphaël Monat, and Antoine Miné

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
This artifact accompanies the submission entitled "DelExp: a Relational Container Abstraction with Applications to Compositional Analysis. It enables to reproduce experimental claims made in the paper. The artifact requires a computer with Docker installed.
Cite as

Milla Valnet, Raphaël Monat, and Antoine Miné. DelExp: A Relational Container Abstraction With Applications to Compositional Analysis (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 15:1-15:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{valnet_et_al:DARTS.12.1.15,
  author =	{Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
  title =	{{DelExp: A Relational Container Abstraction With Applications to Compositional Analysis (Artifact)}},
  pages =	{15:1--15:7},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.15},
  URN =		{urn:nbn:de:0030-drops-261523},
  doi =		{10.4230/DARTS.12.1.15},
  annote =	{Keywords: Static Value Analysis, Functional Programming, Abstract Interpretation}
}
Artifact
Software
DOI: 10.4230/artifacts.25787
Open Verification Dashboard

Authors: Tom Goalard

Abstract
Cite as

Tom Goalard. Open Verification Dashboard (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-25787,
   title = {{Open Verification Dashboard}}, 
   author = {Goalard, Tom},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:f36521d14e7e5034a524502244b9240f7685e760}{\texttt{swh:1:dir:f36521d14e7e5034a524502244b9240f7685e760}} (visited on 2026-06-25)},
   url = {https://github.com/sws-lab/open-verification-dashboard},
   doi = {10.4230/artifacts.25787},
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2026.8
Comparing Transparent Static Analyzers with Open Verification Dashboard

Authors: Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
Given an input program, sound static analyzers compute a list of potential runtime errors in it. However, measuring their precision and comparing their results remains challenging. In this work, we formalize a notion of transparent static analyzers that report the proof obligations they check, including both verified and unverified obligations. This transparent output enables a semantics-directed, fine-grained comparison and the combination of static analyzers. We introduce the Open Verification Dashboard (OVD), which provides a unified interface to aggregate the results of multiple static analyzers. By juxtaposing verified properties and outstanding warnings, OVD highlights coverage gaps, variabilities and inconsistencies across tools. We experimentally evaluate the benefits of OVD on benchmarks from the Competition on Software Verification (SV-COMP). This work paves the way for a static analysis standard for C runtime error reporting.
Cite as

Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat. Comparing Transparent Static Analyzers with Open Verification Dashboard. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 8:1-8:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{goalard_et_al:LIPIcs.ECOOP.2026.8,
  author =	{Goalard, Tom and Holter, Karoliine and Saan, Simmo and Vojdani, Vesal and Monat, Rapha\"{e}l},
  title =	{{Comparing Transparent Static Analyzers with Open Verification Dashboard}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{8:1--8:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.8},
  URN =		{urn:nbn:de:0030-drops-261049},
  doi =		{10.4230/LIPIcs.ECOOP.2026.8},
  annote =	{Keywords: automated static analysis, multi-tool integration, interoperability, proof obligations, result aggregation, verification progress, selectivity metric, reproducibility, dashboard}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2026.14
The Virtual Recency Abstraction: Strong Updates for Abstract Interpreters with Shared State

Authors: Sven Keidel, Raphaël Monat, and Sebastian Erdweg

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
Abstract interpreters enable sound static analysis, but are hard to develop. In recent years, researchers have proposed a component-based approach to developing abstract interpreters, where different parts of the abstract domain (e.g., numeric, call frame, heap) are handled by isolated components. This works well as long as components do not share or expose their internal state: Any state update that is locally sound is also globally sound. However, some abstract domains require shared state, most prominently relational abstract domains, which use symbolic expressions such as 2x + 5 to represent abstract values. As the relational component performs a strong update of x, the abstract value 2x + 5 can change non-monotonically, which breaks soundness. We propose a novel solution to this problem: A virtual recency abstractions that decouples the relational component, supports strong updates, and allows recursion. We prove that the virtual recency abstraction restores soundness: Any shared state wrapped in our virtual recency abstraction may be locally updated non-monotonically, while global soundness persists. We applied our approach to develop the first relational WebAssembly analysis, reusing many components from an existing inter-procedural abstract interpreter. Furthermore, we evaluate the recall, precision, and scalibility of this analysis to demonstrate the practicality of the virtual recency abstraction.
Cite as

Sven Keidel, Raphaël Monat, and Sebastian Erdweg. The Virtual Recency Abstraction: Strong Updates for Abstract Interpreters with Shared State. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 14:1-14:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{keidel_et_al:LIPIcs.ECOOP.2026.14,
  author =	{Keidel, Sven and Monat, Rapha\"{e}l and Erdweg, Sebastian},
  title =	{{The Virtual Recency Abstraction: Strong Updates for Abstract Interpreters with Shared State}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{14:1--14:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.14},
  URN =		{urn:nbn:de:0030-drops-261103},
  doi =		{10.4230/LIPIcs.ECOOP.2026.14},
  annote =	{Keywords: Relational Numerical Analysis, Recency Abstraction}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2026.29
DelExp: A Relational Container Abstraction: with Applications to Compositional Analysis

Authors: Milla Valnet, Raphaël Monat, and Antoine Miné

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
Data containers, such as lists, arrays, trees, etc, raise challenges for program verification. In static analysis by abstract interpretation, one popular approach is summarization: multiple elements of a data structure are abstracted into a single one, favoring performance over precision. This technique is at the core of most container abstractions - from smashing to segmentation - of arrays, lists or algebraic data types. However, summarization approaches are unable to express relations between containers, even when relational numerical abstract domains are used. Our work introduces DelExp, a new domain able to express relations between summarized variables. DelExp can state that the content of a data structure is included in the content of another data structure, up to a given transformation. DelExp is language-agnostic, modular in the abstraction chosen for any other types (integers, strings, functions, etc.), and can be seamlessly combined with existing container abstractions. We show how DelExp allows us to infer precise summaries for compositional analyses of container-manipulating functions in a pure functional language. We present extensions to DelExp supporting polymorphism and higher-order transformations. Our implementation of DelExp within the MOPSA static analysis platform confirms that DelExp works out of the box with pre-existing container abstractions. Our evaluation targets both Python programs manipulating lists and relational summary generation for OCaml functions handling algebraic data types.
Cite as

Milla Valnet, Raphaël Monat, and Antoine Miné. DelExp: A Relational Container Abstraction: with Applications to Compositional Analysis. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 29:1-29:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{valnet_et_al:LIPIcs.ECOOP.2026.29,
  author =	{Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
  title =	{{DelExp: A Relational Container Abstraction: with Applications to Compositional Analysis}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{29:1--29:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.29},
  URN =		{urn:nbn:de:0030-drops-261257},
  doi =		{10.4230/LIPIcs.ECOOP.2026.29},
  annote =	{Keywords: Static Value Analysis, Abstract Interpretation, Functional Programming}
}
Document
Front Matter
DOI: 10.4230/DARTS.11.2.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Karine Even-Mendoza, Raphaël Monat, and Yannick Zakowski

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{evenmendoza_et_al:DARTS.11.2.0,
  author =	{Even-Mendoza, Karine and Monat, Rapha\"{e}l and Zakowski, Yannick},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  pages =	{0:i--0:xii},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Even-Mendoza, Karine and Monat, Rapha\"{e}l and Zakowski, Yannick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.0},
  URN =		{urn:nbn:de:0030-drops-236599},
  doi =		{10.4230/DARTS.11.2.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Artifact
DOI: 10.4230/DARTS.11.2.5
Compositional Static Value Analysis for Higher-Order Numerical Programs (Artifact)

Authors: Milla Valnet, Raphaël Monat, and Antoine Miné

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
This artifact accompanies the submission entitled "Compositional Static Value Analysis for Higher-Order Numerical Programs". It enables to reproduce experimental claims made in the paper. The artifact requires a computer with Docker installed.
Cite as

Milla Valnet, Raphaël Monat, and Antoine Miné. Compositional Static Value Analysis for Higher-Order Numerical Programs (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 5:1-5:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{valnet_et_al:DARTS.11.2.5,
  author =	{Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
  title =	{{Compositional Static Value Analysis for Higher-Order Numerical Programs (Artifact)}},
  pages =	{5:1--5:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.5},
  URN =		{urn:nbn:de:0030-drops-233481},
  doi =		{10.4230/DARTS.11.2.5},
  annote =	{Keywords: Static Value Analysis, Functional Programming, Abstract Interpretation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.28
Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis

Authors: Mamy Razafintsialonina, David Bühler, Antoine Miné, Valentin Perrelle, and Julien Signoles

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Static analysis by means of abstract interpretation is a tool of choice for proving absence of some classes of errors, typically undefined behaviors in C code, in a sound way. However, static analysis tools are hardly integrated in CI/CD processes. One of the main reasons is that they are still time- and memory-expensive to apply after every single patch when developing a program. For solving this issue, incremental static analysis helps developers quickly obtain analysis results after making changes to a program. However, existing approaches are often not guaranteed to be sound, limited to specific analyses, or tied to specific tools. This limits their generalizability and applicability in practice, especially for large and critical software. In this paper, we propose a generic, sound approach to incremental static analysis that is applicable to any abstract interpreter. Our approach leverages the similarity between two versions of a program to soundly reuse previously computed analysis results. We introduce novel methods for summarizing functions and reusing loop invariants. They significantly reduce the cost of reanalysis, while maintaining soundness and a high level of precision. We have formalized our approach, proved it sound, implemented it in Eva, the abstract interpreter of Frama-C, and evaluated it on a set of real-world commits of open-source programs.
Cite as

Mamy Razafintsialonina, David Bühler, Antoine Miné, Valentin Perrelle, and Julien Signoles. Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 28:1-28:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{razafintsialonina_et_al:LIPIcs.ECOOP.2025.28,
  author =	{Razafintsialonina, Mamy and B\"{u}hler, David and Min\'{e}, Antoine and Perrelle, Valentin and Signoles, Julien},
  title =	{{Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{28:1--28:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.28},
  URN =		{urn:nbn:de:0030-drops-233207},
  doi =		{10.4230/LIPIcs.ECOOP.2025.28},
  annote =	{Keywords: Abstract Interpretation, Static Analysis, Incremental Analysis}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.32
Compositional Static Value Analysis for Higher-Order Numerical Programs

Authors: Milla Valnet, Raphaël Monat, and Antoine Miné

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Static analyzers have been successfully developed to detect runtime errors in many languages. However, the automatic analysis of functional languages remains a challenge due to their recursive functions, recursive algebraic data types, and higher-order functions. Classic type systems provide compositional methods that are in general not precise enough to prove the absence of runtime errors such as assertion failures. At the other end of the spectrum, deductive methods are more expressive but may require user guidance to prove invariants. Our work describes a static value analysis by abstract interpretation for a higher-order pure functional language. This analysis provides a sound and automatic approach to discover invariants and prevent assertion and match failures. We have designed a compositional analysis: functions are analyzed only once, at their definition site, generating a summary of their behavior. The summaries can be viewed as input-output relations expressed with relational abstract domains. We present two new abstract domains. A first abstract domain summarizes recursive algebraic data types. A second abstract domain lifts existing disjunctive relational summaries to higher-order by formalizing them as domains able to abstract higher-order functions. Both abstractions are parameterized by the abstractions of basic types (strings, integers, ...). Thanks to this parametric nature, both domains can be combined, allowing the analysis of higher-order functions manipulating algebraic data types and, conversely, algebraic data types using functions as first-class values. We have implemented this analysis in the open-source MOPSA platform. Preliminary evaluation confirms the precision of our approach on a set of 40 handwritten toy programs as well as 20 programs from the state-of-the-art Salto analyzer benchmark.
Cite as

Milla Valnet, Raphaël Monat, and Antoine Miné. Compositional Static Value Analysis for Higher-Order Numerical Programs. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 32:1-32:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{valnet_et_al:LIPIcs.ECOOP.2025.32,
  author =	{Valnet, Milla and Monat, Rapha\"{e}l and Min\'{e}, Antoine},
  title =	{{Compositional Static Value Analysis for Higher-Order Numerical Programs}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{32:1--32:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.32},
  URN =		{urn:nbn:de:0030-drops-233249},
  doi =		{10.4230/LIPIcs.ECOOP.2025.32},
  annote =	{Keywords: Static Value Analysis, Functional Programming, Abstract Interpretation}
}
Document
Front Matter
DOI: 10.4230/DARTS.10.2.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Karine Even-Mendoza and Raphaël Monat

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{evenmendoza_et_al:DARTS.10.2.0,
  author =	{Even-Mendoza, Karine and Monat, Rapha\"{e}l},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  pages =	{0:i--0:xii},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Even-Mendoza, Karine and Monat, Rapha\"{e}l},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.0},
  URN =		{urn:nbn:de:0030-drops-208982},
  doi =		{10.4230/DARTS.10.2.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.11
Static Type Analysis by Abstract Interpretation of Python Programs (Artifact)

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

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
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.
Cite as

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)

Copy BibTex To Clipboard

@Article{monat_et_al:DARTS.6.2.11,
  author =	{Monat, Rapha\"{e}l and Ouadjaout, Abdelraouf and Min\'{e}, Antoine},
  title =	{{Static Type Analysis by Abstract Interpretation of Python Programs (Artifact)}},
  pages =	{11:1--11:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Monat, Rapha\"{e}l and Ouadjaout, Abdelraouf and Min\'{e}, Antoine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.11},
  URN =		{urn:nbn:de:0030-drops-132082},
  doi =		{10.4230/DARTS.6.2.11},
  annote =	{Keywords: Formal Methods, Static Analysis, Abstract Interpretation, Type Analysis, Dynamic Programming Language, Python Semantics}
}
  • Refine by Type
  • 13 Document/PDF
  • 2 Document/HTML
  • 2 Issue
  • 1 Artifact

  • Refine by Publication Year
  • 7 2026
  • 5 2025
  • 2 2024
  • 2 2020

  • Refine by Author
  • 12 Monat, Raphaël
  • 7 Miné, Antoine
  • 4 Valnet, Milla
  • 3 Goalard, Tom
  • 2 Erdweg, Sebastian
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs
  • 7 DARTS

  • Refine by Classification
  • 8 Software and its engineering → Automated static analysis
  • 6 Theory of computation → Program analysis
  • 4 Software and its engineering → Functional languages
  • 2 Software and its engineering
  • 2 Software and its engineering → Semantics
  • Show More...

  • Refine by Keyword
  • 7 Abstract Interpretation
  • 4 Functional Programming
  • 4 Static Value Analysis
  • 3 Static Analysis
  • 2 Conference Organization
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact