Sun 20 Oct 2024 10:00 - 10:30 at San Gabriel - Modularity and Memory Analysis Chair(s): Roberto Giacobazzi

This work presents a sound backward analysis for sufficient pre-conditions inference in C programs, by abstract interpretation. It utilizes the under-approximation abstract operators studied by Milanese and Miné for a purely numeric subset of C, and extends them to support the C memory model. Pointer dereferences are handled with the cell abstraction and dynamic memory allocations with the recency abstraction. A direct usage of the abstract operators proposed in these previous works in an under-approximation framework is not possible as either internally they rely on over-approximated operators (e.g., cell removal) or an extension to this framework is not straightforward (e.g., under-approximating join). In this work we propose new operators that are under-approximating, and on top of this we design a backward semantics. The analysis is implemented in the MOPSA analyzer and its performance is assessed in detection of sufficient pre-conditions for runtime errors in 13,261 C tasks from NIST Juliet test suite.

Sun 20 Oct

Displayed time zone: Pacific Time (US & Canada) change

09:00 - 10:30
Modularity and Memory AnalysisSAS at San Gabriel
Chair(s): Roberto Giacobazzi University of Arizona
09:00
60m
Keynote
Static Analysis Sparsity and Modularity
SAS
Kwangkeun Yi Seoul National University
10:00
30m
Under-approximating Memory Abstractions
SAS
Marco Milanese Sorbonne University, Antoine Miné Sorbonne Université
Pre-print