SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Wed 20 Oct 2021 08:10 - 08:25 at Zurich C - Analysis - mirror Chair(s): Constantin Enea
Wed 20 Oct 2021 16:10 - 16:25 at Zurich C - Analysis Chair(s): Julian Dolby

This paper concerns the scalability challenges of symbolic abstraction: given a formula $\varphi$ in a logic $\mathcal{L}$ and an abstract domain $\mathcal{A}$, find a most precise element in the abstract domain that over-approximates the meaning of $\varphi$. Symbolic abstraction is an important point in the space of abstract interpretation, as it allows for automatically synthesizing the best abstract transformers. However, current techniques for symbolic abstraction can have difficulty delivering on its practical strengths, due to performance issues.

In this work, we introduce two algorithms for the symbolic abstraction of quantifier-free bit-vector formulas, which apply to the bit-vector interval domain and a certain kind of polyhedral domain, respectively. We implement and evaluate the proposed techniques on two machine code analysis clients, namely static memory corruption analysis and constrained random fuzzing. Using a suite of 57,933 queries from the clients, we compare our approach against a diverse group of state-of-the-art algorithms. The experiments show that our algorithms achieve a substantial speedup over existing techniques and illustrate significant precision advantages for the clients. Our work presents strong evidence that symbolic abstraction of numeric domains can be efficient and practical for large and realistic programs.

Wed 20 Oct

Displayed time zone: Central Time (US & Canada) change

07:40 - 09:00
Analysis - mirrorOOPSLA at Zurich C
Chair(s): Constantin Enea University of Paris / IRIF / CNRS
07:40
15m
Talk
Making Pointer Analysis More Precise by Unleashing the Power of Selective Context SensitivityVirtual
OOPSLA
Tian Tan Nanjing University, Yue Li Nanjing University, Xiaoxing Ma Nanjing University, Chang Xu Nanjing University, Yannis Smaragdakis University of Athens
DOI
07:55
15m
Talk
Compacting Points-To Sets through Object ClusteringVirtual
OOPSLA
Mohamad Barbar University of Technology Sydney; CSIRO’s Data61, Yulei Sui University of Technology Sydney
DOI
08:10
15m
Talk
Program Analysis via Efficient Symbolic AbstractionVirtual
OOPSLA
Peisen Yao Hong Kong University of Science and Technology; Ant Group, Qingkai Shi Ant Group, Heqing Huang Hong Kong University of Science and Technology, Charles Zhang Hong Kong University of Science and Technology
DOI
08:25
15m
Talk
JavaDL: Automatically Incrementalizing Java Bug Pattern DetectionVirtual
OOPSLA
Alexandru Dura Lund University, Christoph Reichenbach Lund University, Emma Söderberg Lund University
DOI
08:40
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA

15:40 - 17:00
AnalysisOOPSLA at Zurich C -8h
Chair(s): Julian Dolby IBM Research, USA
15:40
15m
Talk
Making Pointer Analysis More Precise by Unleashing the Power of Selective Context SensitivityVirtual
OOPSLA
Tian Tan Nanjing University, Yue Li Nanjing University, Xiaoxing Ma Nanjing University, Chang Xu Nanjing University, Yannis Smaragdakis University of Athens
DOI
15:55
15m
Talk
Compacting Points-To Sets through Object ClusteringVirtual
OOPSLA
Mohamad Barbar University of Technology Sydney; CSIRO’s Data61, Yulei Sui University of Technology Sydney
DOI
16:10
15m
Talk
Program Analysis via Efficient Symbolic AbstractionVirtual
OOPSLA
Peisen Yao Hong Kong University of Science and Technology; Ant Group, Qingkai Shi Ant Group, Heqing Huang Hong Kong University of Science and Technology, Charles Zhang Hong Kong University of Science and Technology
DOI
16:25
15m
Talk
JavaDL: Automatically Incrementalizing Java Bug Pattern DetectionVirtual
OOPSLA
Alexandru Dura Lund University, Christoph Reichenbach Lund University, Emma Söderberg Lund University
DOI
16:40
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA