13 Search Results for "Miné, Antoine"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.8
Model Checking as Program Verification by Abstract Interpretation

Authors: Paolo Baldan, Roberto Bruni, Francesco Ranzato, and Diletta Rigo

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Abstract interpretation offers a powerful toolset for static analysis, tackling precision, complexity and state-explosion issues. In the literature, state partitioning abstractions based on (bi)simulation and property-preserving state relations have been successfully applied to abstract model checking. Here, we pursue a different track in which model checking is seen as an instance of program verification. To this purpose, we introduce a suitable language - called MOKA (for MOdel checking as abstract interpretation of 𝖪leene 𝖠lgebras) - which is used to encode temporal formulae as programs. In particular, we show that (universal fragments of) temporal logics, such as ACTL or, more generally, universal μ-calculus can be transformed into MOKA programs. Such programs return all and only the initial states which violate the formula. By applying abstract interpretation to MOKA programs, we pave the way for reusing more general abstractions than partitions as well as for tuning the precision of the abstraction to remove or avoid false alarms. We show how to perform model checking via a program logic that combines under-approximation and abstract interpretation analysis to avoid false alarms. The notion of locally complete abstraction is used to dynamically improve the analysis precision via counterexample-guided domain refinement.
Cite as

Paolo Baldan, Roberto Bruni, Francesco Ranzato, and Diletta Rigo. Model Checking as Program Verification by Abstract Interpretation. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CONCUR.2025.8,
  author =	{Baldan, Paolo and Bruni, Roberto and Ranzato, Francesco and Rigo, Diletta},
  title =	{{Model Checking as Program Verification by Abstract Interpretation}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.8},
  URN =		{urn:nbn:de:0030-drops-239583},
  doi =		{10.4230/LIPIcs.CONCUR.2025.8},
  annote =	{Keywords: ACTL, \mu-calculus, model checking, abstract interpretation, program analysis, local completeness, abstract interpretation repair, domain refinement, Kleene algebra with tests}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.40
An Efficient and Uniform CSP Solution Generator Generator

Authors: Ghiles Ziat and Martin Pépin

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Constraint-based random testing is a powerful technique which aims at generating random test cases to verify functional properties of a program. Its objective is to determine whether a function satisfies a given property for every possible input. This approach requires firstly defining the property to satisfy, then secondly to provide a "generator of inputs" able to feed the program with the inputs generated. Besides, function inputs often need to satisfy certain constraints to ensure the function operates correctly, which makes the crafting of such a generator a hard task. In this paper, we are interested in the problem of manufacturing a uniform and efficient generator for the solutions of a CSP. In order to do that, we propose a specialized solving method that produces a well-suited representation for random sampling. Our solving method employs a dedicated propagation scheme based on the hypergraph representation of a CSP, and a custom split heuristic called birdge-first that emphasizes the interests of our propagation scheme. The generators we build are general enough to handle a wide range of use-cases. They are moreover uniform by construction, iterative and self-improving. We present a prototype built upon the AbSolute constraint solving library and demonstrate its performances on several realistic examples.
Cite as

Ghiles Ziat and Martin Pépin. An Efficient and Uniform CSP Solution Generator Generator. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ziat_et_al:LIPIcs.CP.2025.40,
  author =	{Ziat, Ghiles and P\'{e}pin, Martin},
  title =	{{An Efficient and Uniform CSP Solution Generator Generator}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{40:1--40:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.40},
  URN =		{urn:nbn:de:0030-drops-239010},
  doi =		{10.4230/LIPIcs.CP.2025.40},
  annote =	{Keywords: Constraint Programming, Property-based Testing}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.34
Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering

Authors: Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui

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

Abstract
Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using semantic functions over ordered sets along a program’s control flow graph (CFG). To facilitate fixpoint computation in abstract interpretation, weak topological ordering (WTO) is an effective strategy for handling loops, as it identifies strategic control points in the CFG where widening and narrowing operations should be applied. However, existing abstract interpreters still face challenges when extending WTO computation in the presence of recursive programs. Computing a precise whole-program WTO requires full context-sensitive analysis which is not scalable for large programs, while context-insensitive analysis introduces spurious cycles that compromise precision. Current approaches either ignore recursion (resulting in unsoundness) or rely on conservative approximations, sacrificing precision by adopting the greatest elements of abstract domains and applying widening at function boundaries without subsequent narrowing refinements. These can lead to undesired results for downstream tasks, such as bug detection. To address the above limitations, we present RecTopo, a new technique to boost the efficiency of precise abstract interpretation in the presence of recursive programs through interprocedural weak topological ordering (IWTO). Rather than pursuing an expensive whole-program WTO analysis, RecTopo employs an on-demand approach that strategically decomposes programs at recursion boundaries and constructs targeted IWTOs for each recursive component. RecTopo dissects and analyzes (nested) recursions through interleaved widening and narrowing operations. This approach enables precise control over interpretation ordering within recursive structures while eliminating spurious recursions through systematic correlation of control flow and call graphs. We implemented RecTopo and evaluated its effectiveness using an assertion-based checking client focused on buffer overflow detection, comparing it against three popular open-source abstract interpreters (IKOS, Clam, CSA). The experiments on 8312 programs from the NIST dataset demonstrate that, on average, RecTopo is 31.99% more precise and achieves a 17.49% higher recall rate compared to three other tools. Moreover, RecTopo exhibits an average precision improvement of 46.51% and a higher recall rate of 32.98% compared to our baselines across ten large open-source projects. Further ablation studies reveal that IWTO reduces spurious widening operations compared to whole-program WTO, resulting in a 12.83% reduction in analysis time.
Cite as

Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui. Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 34:1-34:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.ECOOP.2025.34,
  author =	{Yang, Jiawei and Cheng, Xiao and Chang, Bor-Yuh Evan and Luo, Xiapu and Sui, Yulei},
  title =	{{Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{34:1--34:31},
  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.34},
  URN =		{urn:nbn:de:0030-drops-233265},
  doi =		{10.4230/LIPIcs.ECOOP.2025.34},
  annote =	{Keywords: Abstract interpretation, recursion, weak topological ordering}
}
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
Experience Paper
DOI: 10.4230/LIPIcs.ECOOP.2025.37
RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)

Authors: Tomáš Dacík and Tomáš Vojnar

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

Abstract
We present RacerF, a novel static analyser for thread-modular data race detection. The approach behind RacerF exploits static analysis of sequential program behaviour whose results are generalised for multi-threaded programs using a combination of lightweight under- and over-approximating methods. The tool is implemented as a plugin of the Frama-C platform and can leverage several analysis backends, most notably the Frama-C’s abstract interpreter EVA. Although our methods are mostly heuristic without providing formal guarantees, our experimental evaluation shows that even for intricate programs, RacerF can provide very precise results competitive with more heavyweight approaches while being faster than them.
Cite as

Tomáš Dacík and Tomáš Vojnar. RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dacik_et_al:LIPIcs.ECOOP.2025.37,
  author =	{Dac{\'\i}k, Tom\'{a}\v{s} and Vojnar, Tom\'{a}\v{s}},
  title =	{{RacerF: Lightweight Static Data Race Detection for C Code}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{37:1--37:19},
  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.37},
  URN =		{urn:nbn:de:0030-drops-233298},
  doi =		{10.4230/LIPIcs.ECOOP.2025.37},
  annote =	{Keywords: concurrency, data race detection, static analysis}
}
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
Artifact
DOI: 10.4230/DARTS.11.2.15
Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis (Artifact)

Authors: Mamy Razafintsialonina, David Bühler, and Valentin Perrelle

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 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 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, and Valentin Perrelle. Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 15:1-15:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{razafintsialonina_et_al:DARTS.11.2.15,
  author =	{Razafintsialonina, Mamy and B\"{u}hler, David and Perrelle, Valentin},
  title =	{{Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis (Artifact)}},
  pages =	{15:1--15:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Razafintsialonina, Mamy and B\"{u}hler, David and Perrelle, Valentin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.15},
  URN =		{urn:nbn:de:0030-drops-233586},
  doi =		{10.4230/DARTS.11.2.15},
  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
DOI: 10.4230/DagRep.13.7.66
Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281)

Authors: Arie Gurfinkel, Isabella Mastroeni, Antoine Miné, Peter Müller, and Anna Becchi

Published in: Dagstuhl Reports, Volume 13, Issue 7 (2024)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23281 "Theoretical Advances and Emerging Applications in Abstract Interpretation." Abstract Interpretation (AI) is a theory of the approximation of program semantics. Since its introduction in the 70s, it lead to insights into theoretical research in semantics, a rich and robust mathematical framework to discuss about semantic approximation and program analysis, and the design of effective program analysis tools that are now routinely used in this industry. The seminar brought together academic and industrial partners to assess the state of the art in AI as well as discuss its future. It considered its foundational aspects, connections with other formal methods, emergent applications, user needs in program verification, tool design and evaluation, as well as educational aspects and community management. Its goal was to collect new ideas and new perspectives on all these aspects of AI in order to pave the way for new applications.
Cite as

Arie Gurfinkel, Isabella Mastroeni, Antoine Miné, Peter Müller, and Anna Becchi. Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281). In Dagstuhl Reports, Volume 13, Issue 7, pp. 66-95, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{gurfinkel_et_al:DagRep.13.7.66,
  author =	{Gurfinkel, Arie and Mastroeni, Isabella and Min\'{e}, Antoine and M\"{u}ller, Peter and Becchi, Anna},
  title =	{{Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281)}},
  pages =	{66--95},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{7},
  editor =	{Gurfinkel, Arie and Mastroeni, Isabella and Min\'{e}, Antoine and M\"{u}ller, Peter and Becchi, Anna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.7.66},
  URN =		{urn:nbn:de:0030-drops-197759},
  doi =		{10.4230/DagRep.13.7.66},
  annote =	{Keywords: abstract domains, abstract interpretation, program semantics, program verification, static program analysis}
}
Document
DOI: 10.4230/LITES.8.2.1
Safety Verification of Networked Control Systems by Complex Zonotopes

Authors: Arvind Adimoolam and Thao Dang

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
Networked control systems (NCS) are widely used in real world applications because of their advantages, such as remote operability and reduced installation costs. However, they are prone to various inaccuracies in execution like delays, packet dropouts, inaccurate sensing and quantization errors. To ensure safety of NCS, their models have to be verified under the consideration of aforementioned uncertainties. In this paper, we tackle the problem of verifying safety of models of NCS under uncertain sampling time, inaccurate output measurement or estimation, and unknown disturbance input. Unbounded-time safety verification requires approximation of reachable sets by invariants, whose computation involves set operations. For uncertain linear dynamics, two important set operations for invariant computation are linear transformation and Minkowski sum operations. Zonotopes have the advantage that linear transformation and Minkowski sum operations can be efficiently approximated. However, they can not encode directions of convergence of trajectories along complex eigenvectors, which is closely related to encoding invariants. Therefore, we extend zonotopes to the complex valued domain by a representation called complex zonotope, which can capture contraction along complex eigenvectors for determining invariants. We prove a related mathematical result that in case of accurate feedback sampling, a complex zonotope will represent an invariant for a stable NCS. In addition, we propose an algorithm to verify the general case based on complex zonotopes, when there is uncertainty in sampling time and in input. We demonstrate the efficiency of our algorithm on benchmark examples and compare it with a state-of-the-art verification tool.
Cite as

Arvind Adimoolam and Thao Dang. Safety Verification of Networked Control Systems by Complex Zonotopes. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 01:1-01:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{adimoolam_et_al:LITES.8.2.1,
  author =	{Adimoolam, Arvind and Dang, Thao},
  title =	{{Safety Verification of Networked Control Systems by Complex Zonotopes}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{01:1--01:22},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.1},
  URN =		{urn:nbn:de:0030-drops-192934},
  doi =		{10.4230/LITES.8.2.1},
  annote =	{Keywords: Safety Verification, Networked Control System, Reachability Analysis, Complex Zonotope}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.7
Abstract Interpretation, Symbolic Execution and Constraints

Authors: Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
Abstract interpretation is a static analysis framework for sound over-approximation of all possible runtime states of a program. Symbolic execution is a framework for reachability analysis which tries to explore all possible execution paths of a program. A shared feature between abstract interpretation and symbolic execution is that each - implicitly or explicitly - maintains constraints during execution, in the form of invariants or path conditions. We investigate the relations between the worlds of abstract interpretation, symbolic execution and constraint solving, to expose potential synergies.
Cite as

Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. Abstract Interpretation, Symbolic Execution and Constraints. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{amadini_et_al:OASIcs.Gabbrielli.7,
  author =	{Amadini, Roberto and Gange, Graeme and Schachte, Peter and S{\o}ndergaard, Harald and Stuckey, Peter J.},
  title =	{{Abstract Interpretation, Symbolic Execution and Constraints}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{7:1--7:19},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.7},
  URN =		{urn:nbn:de:0030-drops-132294},
  doi =		{10.4230/OASIcs.Gabbrielli.7},
  annote =	{Keywords: Abstract interpretation, symbolic execution, constraint solving, dynamic analysis, static analysis}
}
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}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.17
Static Type Analysis by Abstract Interpretation of Python Programs

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

Published in: LIPIcs, Volume 166, 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. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 17:1-17:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{monat_et_al:LIPIcs.ECOOP.2020.17,
  author =	{Monat, Rapha\"{e}l and Ouadjaout, Abdelraouf and Min\'{e}, Antoine},
  title =	{{Static Type Analysis by Abstract Interpretation of Python Programs}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{17:1--17:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.17},
  URN =		{urn:nbn:de:0030-drops-131748},
  doi =		{10.4230/LIPIcs.ECOOP.2020.17},
  annote =	{Keywords: Formal Methods, Static Analysis, Abstract Interpretation, Type Analysis, Dynamic Programming Language, Python Semantics}
}
  • Refine by Type
  • 13 Document/PDF
  • 7 Document/HTML

  • Refine by Publication Year
  • 8 2025
  • 1 2024
  • 1 2022
  • 3 2020

  • Refine by Author
  • 6 Miné, Antoine
  • 4 Monat, Raphaël
  • 2 Bühler, David
  • 2 Ouadjaout, Abdelraouf
  • 2 Perrelle, Valentin
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs
  • 1 OASIcs
  • 3 DARTS
  • 1 LITES
  • 1 DagRep

  • Refine by Classification
  • 6 Theory of computation → Program analysis
  • 4 Software and its engineering → Automated static analysis
  • 3 Software and its engineering → Formal methods
  • 3 Software and its engineering → Software verification and validation
  • 2 Software and its engineering → Functional languages
  • Show More...

  • Refine by Keyword
  • 6 Abstract Interpretation
  • 4 Static Analysis
  • 2 Abstract interpretation
  • 2 Dynamic Programming Language
  • 2 Formal Methods
  • 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