Under-approximating memory abstractions
This work presents a sound backward analysis for sufficient pre-conditions inference in C programs, by abstract interpretation. It builds upon previous works done 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…
