ECOOP 2025
Mon 30 June - Fri 4 July 2025 Bergen, Norway
Wed 2 Jul 2025 11:48 - 12:09 at Auditorium M003 - Program Analysis and Verification Chair(s): Einar Broch Johnsen

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.

Wed 2 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:45 - 12:30
Program Analysis and VerificationTechnical Papers at Auditorium M003
Chair(s): Einar Broch Johnsen University of Oslo
10:45
21m
Talk
Bottom-up Synthesis of Memory Mutations with Separation Logic
Technical Papers
Kasra Ferdowsi University of California at San Diego, Hila Peleg Technion
11:06
21m
Talk
Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
Technical Papers
Guanqin Zhang University of New South Wales & CSIRO's Data61, Kota Fukuda Kyushu University, Zhenya Zhang Kyushu University, Japan, ‪H M N Dilum Bandara Data61, CSIRO, Shiping Chen Data61 at CSIRO, Australia / UNSW, Australia, Jianjun Zhao Kyushu University, Yulei Sui University of New South Wales
Link to publication Pre-print Media Attached
11:27
21m
Talk
IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL
Technical Papers
Matt Griffin Imperial College London, Brijesh Dongol University of Surrey, Azalea Raad Imperial College London
11:48
21m
Talk
Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis
Technical Papers
Mamy Razafintsialonina Université Paris-Saclay, CEA, List, Palaiseau / Sorbonne Université, CNRS, LIP6, Paris, David Bühler Université Paris-Saclay, CEA, List, Palaiseau, Antoine Miné Sorbonne Université, Valentin Perrelle Université Paris-Saclay, CEA, List, Palaiseau, Julien Signoles Université Paris-Saclay, CEA, List
12:09
21m
Talk
RacerF: Lightweight Static Data Race Detection for C Code
Technical Papers
Tomáš Dacík Faculty of Information Technology, Brno University of Technology, Tomas Vojnar Masaryk University
:
:
:
: