Search Results

Documents authored by Perrelle, Valentin

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
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.FSTTCS.2021.51
Concrete Categorical Model of a Quantum Circuit Description Language with Measurement

Authors: Dongho Lee, Valentin Perrelle, Benoît Valiron, and Zhaowei Xu

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
In this paper, we introduce dynamic lifting to a quantum circuit-description language, following the Proto-Quipper language approach. Dynamic lifting allows programs to transfer the result of measuring quantum data - qubits - into classical data - booleans -. We propose a type system and an operational semantics for the language and we state safety properties. Next, we introduce a concrete categorical semantics for the proposed language, basing our approach on a recent model from Rios&Selinger for Proto-Quipper-M. Our approach is to construct on top of a concrete category of circuits with measurements a Kleisli category, capturing as a side effect the action of retrieving classical content out of a quantum memory. We then show a soundness result for this semantics.
Cite as

Dongho Lee, Valentin Perrelle, Benoît Valiron, and Zhaowei Xu. Concrete Categorical Model of a Quantum Circuit Description Language with Measurement. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 51:1-51:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{lee_et_al:LIPIcs.FSTTCS.2021.51,
  author =	{Lee, Dongho and Perrelle, Valentin and Valiron, Beno\^{i}t and Xu, Zhaowei},
  title =	{{Concrete Categorical Model of a Quantum Circuit Description Language with Measurement}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{51:1--51:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.51},
  URN =		{urn:nbn:de:0030-drops-155627},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.51},
  annote =	{Keywords: Categorical semantics, Operational semantics, Quantum circuit description language}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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