Many abstract interpretation-based analyses focus on numeric
properties or heap properties, but not both. For example, Calcagno et
al. [1]} uses separation logic to create a
compositional, bottom-up heap analysis. Their client analysis for Java
checks for NULL pointers [2]}, but not out-of-bounds array
indexes. Conversely, the PAGAI analyzer
[3]} for LLVM explores abstract interpretation
algorithms for precise invariants of numeric variables, but ignores
the heap (soundly treating heap locations as \(\top \) ).
