A Practical Construction for Decomposing Numerical Abstract Domains
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 JanDisplayed time zone: Tijuana, Baja California change
13:30 - 15:20
Program Analysis IIResearch Papers at Bunker Hill
Chair(s): Işil Dillig UT Austin
Benjamin Delaware Purdue University
|Refinement Reflection: Complete Verification with SMT|
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
|Non-Linear Reasoning For Invariant Synthesis|
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.
|A Practical Construction for Decomposing Numerical Abstract Domains|
Gagandeep Singh , Markus Püschel ETH Zürich, Martin Vechev ETH Zürich
|Verifying Equivalence of Database-Driven Applications|
Yuepeng Wang University of Texas at Austin, Işil Dillig UT Austin, Shuvendu K. Lahiri Microsoft Research, William Cook University of Texas at Austin