Despite decades of progress, static analysis tools still have great difficulty
dealing with programs that combine arithmetic, loops, dynamic memory
allocation, and linked data structures. In this paper we draw attention to two
fundamental reasons for this difficulty: First, typical underlying program
abstractions are low-level and inherently scalar, characterizing
compound entities like data structures or results computed through iteration
only indirectly. Second, to ensure termination, analyses typically project
away the dimension of time, and merge information per program point, which
incurs a loss in precision.

As a remedy, we propose to make collective operations first-class in program
analysis – inspired by $\Sigma$-notation in mathematics, and also by the
success of high-level intermediate languages based on @map/reduce@ operations
in program generators and aggressive optimizing compilers for domain-specific
languages (DSLs). We further propose a novel structured heap abstraction that
preserves a symbolic dimension of time, reflecting the program's loop structure
and thus unambiguously correlating multiple temporal points in the dynamic
execution with a single point in the program text.

This paper presents a formal model, based on a high-level intermediate analysis
language, a practical realization in a prototype tool that analyzes C code, and
an experimental evaluation that demonstrates competitive results on a series of
benchmarks. Remarkably, our implementation achieves these results in a fully
semantics-preserving strongest-postcondition model, which is a worst-case for
analysis/verification. The underlying ideas, however, are not tied to this
model and would equally apply in other settings, e.g., demand-driven invariant
inference in a weakest-precondition model. Given its semantics-preserving
nature, our implementation is not limited to analysis for verification, but can
also check program equivalence, and translate legacy C code to high-performance
DSLs.