Making numerical program analysis fast

Gagandeep Singh, Markus Püschel, Martin Vechev

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 four published static analyzers showing massive speedups for the time spent in Octagon analysis (e.g., up to 146x) as well as significant end-to-end program analysis speedups (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.

Original languageEnglish (US)
Title of host publicationPLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsSteve Blackburn, David Grove
PublisherAssociation for Computing Machinery
Number of pages11
ISBN (Electronic)9781450334686
StatePublished - Jun 2015
Externally publishedYes
Event36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 - Portland, United States
Duration: Jun 13 2015Jun 17 2015

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)


Other36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015
Country/TerritoryUnited States


  • Fast numerical program analysis
  • Octagon abstract domain
  • Octagon closure algorithm
  • Octagon decomposition
  • Sparse octagon operators
  • Vectorized octagon operators

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Making numerical program analysis fast'. Together they form a unique fingerprint.

Cite this