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

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 Σ-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.

This program is tentative and subject to change.

Wed 23 Oct

splash-2019-oopsla
16:00 - 17:30: OOPSLA - Analysis at Olympia
splash-2019-oopsla16:00 - 16:22
Talk
Jingbo LuUNSW Sydney, Jingling XueUNSW Sydney
splash-2019-oopsla16:22 - 16:45
Talk
Gregory EssertelPurdue University, Guannan WeiPurdue University, Tiark RompfPurdue University
splash-2019-oopsla16:45 - 17:07
Talk
Milijana SurbatovichCarnegie Mellon University, Limin JiaCarnegie Mellon University, Brandon LuciaCarnegie Mellon University
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