This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Sun 20 OctDisplayed time zone: Pacific Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | Static Analysis Sparsity and Modularity SAS Kwangkeun Yi Seoul National University | ||
10:00 30m | Under-approximating Memory Abstractions SAS Pre-print |