POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 11:45 - 12:10 at Amphitheater 44 - Abstract Interpretation Chair(s): Isabella Mastroeni

Numerical abstract domains are an important ingredient of modern static analyzers used for verifying critical program properties (e.g., absence of buffer overflow or memory safety). Among the many numerical domains introduced over the years, Polyhedra is the most expressive one, but also the most expensive: it has worst-case exponential space and time complexity. As a consequence, static analysis with the Polyhedra domain is thought to be impractical when applied to large scale, real world programs.

In this paper, we present a new approach and a complete implementation for speeding up Polyhedra domain analysis. Our approach does not lose precision, and for many practical cases, is orders of magnitude faster than state-of-the-art solutions. The key insight is that polyhedra arising during static analysis can usually be kept decomposed during the analysis, thus considerably reducing the overall complexity.

We first present the theory underlying our approach, which identifies the interaction between partitions of variables and domain operators. Based on the theory we develop new algorithms for these operators that work with decomposed polyhedra. We implemented these algorithms using the same interface as existing libraries, thus enabling static analyzers to use our implementation with little effort. In our evaluation, we analyze large benchmarks from the popular software verification competition, including Linux device drivers with over 50K lines of code. Our experimental results demonstrate massive gains in both space and time: we show end-to-end speedups of two to five orders of magnitude compared to state-of-the-art Polyhedra implementations as well as significant memory gains, on all larger benchmarks.

As a result, we believe this work is an important step in making the Polyhedra abstract domain practically usable for handling large, real-world programs.

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: Abstract InterpretationPOPL at Amphitheater 44
Chair(s): Isabella MastroeniUniversity of Verona, Italy
10:30 - 10:55
Jade AlglaveUniversity College London, Patrick CousotNew York University
10:55 - 11:20
Kimball GermaneUniversity of Utah, Matthew MightUniversity of Utah; Harvard Medical School; The White House
11:20 - 11:45
Huisong LiINRIA/CNRS/ENS/PSL*, François BérengerINRIA/CNRS/ENS/PSL*, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Xavier RivalINRIA/CNRS/ENS Paris
11:45 - 12:10
Gagandeep SinghETH Zurich, Switzerland, Markus PüschelETH Zurich, Martin VechevETH Zurich