Fri 12 Jan 2018 14:30 - 14:55 at Bunker Hill - Program Analysis II Chair(s): Isil Dillig

Numerical abstract domains such as Polyhedra, Octahedron, Octagon, Interval, and others are an essential component of static program analysis. The choice of domain offers a performance/precision tradeoff ranging from cheap and imprecise (Interval) to expensive and precise (Polyhedra). Recently, significant speedups were achieved for Octagon and Polyhedra by manually decomposing their transformers to work with the Cartesian product of projections associated with partitions of the variable set. While practically useful, this manual process is extremely time consuming, error-prone and has to be applied from scratch for every domain.

In this paper, we present a novel approach that can soundly decompose any sub-polyhedra domain. Unlike prior work, the method is generic in nature and does not require changes to the original abstract transformers or additional manual effort per domain. Further, it presents guarantees on the partitions achievable by each decomposed transformer. In general, our method achieves finer partitions than prior work.

We implemented our approach and applied it to the domains of Zones, Octagon, and Polyhedra. We then compared the performance of the decomposed transformers obtained with our generic method versus state-of-the art PPL and the faster ELINA (which uses manual decomposition). Against the latter we demonstrate finer partitions and an associated speedup of about 2x on average. Our results indicate that the construction presented in this work is a viable method for improving the performance of numerical domains. It enables designers of abstract domains to benefit from decomposition without re-writing all of their transformers from scratch (as required by prior methods).

Fri 12 Jan
Times are displayed in time zone: Tijuana, Baja California change

13:30 - 15:20: Program Analysis IIResearch Papers at Bunker Hill
Chair(s): Isil DilligUT Austin
13:30 - 13:40
SRC Awards
Research Papers
Benjamin DelawarePurdue University
13:30 - 13:52
Refinement Reflection: Complete Verification with SMT
Research Papers
Niki VazouUniversity of Maryland, Anish TondwalkarUCSD, Vikraman Choudhury, Ryan ScottIndiana University, Ryan R. NewtonIndiana University, Philip WadlerUniversity of Edinburgh, UK, Ranjit JhalaUniversity of California, San Diego
14:05 - 14:30
Non-Linear Reasoning For Invariant Synthesis
Research Papers
Zachary KincaidPrinceton University, John CyphertUniversity of Wisconsin - Madison, Jason BreckUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.
14:30 - 14:55
A Practical Construction for Decomposing Numerical Abstract Domains
Research Papers
14:55 - 15:20
Verifying Equivalence of Database-Driven Applications
Research Papers
Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Shuvendu K. LahiriMicrosoft Research, William CookUniversity of Texas at Austin