Search Results

Documents authored by Valnet, Milla

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
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}
}
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
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}
}
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