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

Displayed time zone: Tijuana, Baja California change

13:30 - 15:20
Program Analysis IIResearch Papers at Bunker Hill
Chair(s): Isil Dillig UT Austin
13:30
10m
Awards
SRC Awards
Research Papers
Benjamin Delaware Purdue University
13:30
22m
Talk
Refinement Reflection: Complete Verification with SMT
Research Papers
Niki Vazou University of Maryland, Anish Tondwalkar UCSD, Vikraman Choudhury , Ryan Scott Indiana University, Ryan R. Newton Indiana University, Philip Wadler University of Edinburgh, UK, Ranjit Jhala University of California, San Diego
14:05
25m
Talk
Non-Linear Reasoning For Invariant Synthesis
Research Papers
Zachary Kincaid Princeton University, John Cyphert University of Wisconsin - Madison, Jason Breck University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
14:30
25m
Talk
A Practical Construction for Decomposing Numerical Abstract Domains
Research Papers
Gagandeep Singh , Markus Püschel ETH Zürich, Martin Vechev ETH Zürich
14:55
25m
Talk
Verifying Equivalence of Database-Driven Applications
Research Papers
Yuepeng Wang University of Texas at Austin, Isil Dillig UT Austin, Shuvendu Lahiri Microsoft Research, William Cook University of Texas at Austin