| Title: |
DelExp: a Relational Container Abstraction with Applications to Compositional Analysis |
| Authors: |
Valnet, Milla; Monat, Raphaël; Miné, Antoine |
| Contributors: |
Algorithmes, Programmes et Résolution (APR); LIP6; Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS); Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires (SYCOMORES); Centre Inria de l'Université de Lille; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL); Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS); Institut universitaire de France (IUF); Ministère de l'Education nationale, de l’Enseignement supérieur et de la Recherche (M.E.N.E.S.R.) |
| Source: |
https://inria.hal.science/hal-05563571 ; 2026. |
| Publisher Information: |
CCSD |
| Publication Year: |
2026 |
| Subject Terms: |
2012 ACM Subject Classification Software and its engineering → Automated static analysis Theory of computation → Program analysis Software and its engineering → Functional languages Static Value Analysis; Abstract Interpretation; Functional Programming Digital Object Identifier 10.4230/LIPIcs; 2012 ACM Subject Classification Software and its engineering → Automated static analysis; Theory of computation → Program analysis; Software and its engineering → Functional languages Static Value Analysis; [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] |
| Description: |
International audience ; 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. |
| Document Type: |
report |
| Language: |
English |
| Availability: |
https://inria.hal.science/hal-05563571; https://inria.hal.science/hal-05563571v1/document; https://inria.hal.science/hal-05563571v1/file/ecoop26.pdf |
| Rights: |
https://creativecommons.org/licenses/by/4.0/ ; info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.5587EE |
| Database: |
BASE |