Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis
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 JulDisplayed 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 21mTalk | Bottom-up Synthesis of Memory Mutations with Separation Logic Technical Papers | ||
11:06 21mTalk | 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 21mTalk | 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 21mTalk | 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 21mTalk | 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 |