Tue 16 Jun 2015 14:50 - 15:15 at PLDI Main BLUE (Portland 254-255) - Analysis Chair(s): Yannis Smaragdakis

Numerical abstract domains are a fundamental component in modern static program analysis and are used in a wide range of scenarios (e.g. computing array bounds, disjointness, etc). However, analysis with these domains can be very expensive, deeply affecting the scalability and practical applicability of the static analysis. Hence, it is critical to ensure that these domains are made highly efficient.

In this work, we present a complete approach for optimizing the performance of the Octagon numerical abstract domain, a domain shown to be particularly effective in practice. Our optimization approach is based on two key insights: i) the ability to perform online decomposition of the octagons leading to a massive reduction in operation counts, and ii) leveraging classic performance optimizations from linear algebra such as vectorization, locality of reference, scalar replacement and others, for improving the key bottlenecks of the domain. Applying these ideas, we designed new algorithms for the core Octagon operators with better asymptotic runtime than prior work and combined them with the optimization techniques to achieve high actual performance. We implemented our approach in the Octagon operators exported by the popular APRON C library, thus enabling existing static analyzers using APRON to immediately benefit from our work.

To demonstrate the performance benefits of our approach, we evaluated our framework on three published static analyzers showing massive speed-ups for the time spent in Octagon analysis (e.g., up to 146x) as well as significant end-to-end program analysis speed-ups (up to 18.7x). Based on these results, we believe that our framework can serve as a new basis for static analysis with the Octagon numerical domain.

PLDI 2015 Artifact Evaluated Badge

Tue 16 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:40
AnalysisResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Yannis Smaragdakis University of Athens
14:00
25m
Talk
DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs
Research Papers
Akash Lal Microsoft Research India, Shaz Qadeer Microsoft Research
Media Attached File Attached
14:25
25m
Talk
Exploring and Enforcing Security Guarantees via Program Dependence Graphs
Research Papers
Andrew Johnson Harvard University, Lucas Waye Harvard University, Scott Moore Harvard University, Stephen Chong Harvard University
Media Attached
14:50
25m
Talk
Making Numerical Program Analysis Fast
Research Papers
Gagandeep Singh ETH Zurich, Switzerland, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich
Media Attached
15:15
25m
Talk
Tree Dependence Analysis
Research Papers
Yusheng Weijiang Purdue University, Shruthi Balakrishna Purdue University, Jianqiao Liu Purdue University, Milind Kulkarni Purdue University
Media Attached