Abstract by Jame Wasson
Precise Pointer Arithmetic in Abstract Interpretation
C is powerful because it gives programmers direct control over memory.
This control makes it the language of choice for many time- or memory-critical programs
but leads to subtle memory errors and undefined behaviors that often go unnoticed.
Not only is it useful to detect or disprove these errors, the ability to reason about these errors is a prerequisite to reasoning about other properties of C programs that use pointer arithmetic.
Pointer arithmetic has far-reaching effects but achieves them through very limited operations: addition and subtraction.
Additionally, memory can only be allocated in finite, discrete regions.
As a result, it is possible to create an abstract interpreter with an appropriately limited memory model that is faithful to these operations.
With the ability to reason about pointer arithmetic, it is also possible to reason about other properties of C.