Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Wed 23 Oct 2019 16:22 - 16:45 at Olympia - Analysis Chair(s): Jan Vitek

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.

Wed 23 Oct

splash-2019-oopsla
16:00 - 17:30: OOPSLA - Analysis at Olympia
Chair(s): Jan VitekNortheastern University
splash-2019-oopsla16:00 - 16:22
Talk
Jingbo LuUNSW Sydney, Jingling XueUNSW Sydney
DOI
splash-2019-oopsla16:22 - 16:45
Talk
Gregory EssertelPurdue University, Guannan WeiPurdue University, Tiark RompfPurdue University
DOI
splash-2019-oopsla16:45 - 17:07
Talk
Milijana SurbatovichCarnegie Mellon University, Limin JiaCarnegie Mellon University, Brandon LuciaCarnegie Mellon University
DOI
splash-2019-oopsla17:07 - 17:30
Talk
Emma ToschUniversity of Massachusetts Amherst, Eytan BakshyFacebook, Inc., Emery BergerUniversity of Massachusetts Amherst, David JensenUniversity of Massachusetts Amherst, Eliot MossUniversity of Massachusetts Amherst
DOI