SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Sun 17 Oct 2021 09:00 - 09:15 at Zurich B - Session 1A Chair(s): Cezara Drăgoi
Sun 17 Oct 2021 17:00 - 17:15 at Zurich B - Session 1A Chair(s): Kedar Namjoshi

Static program analysis uses sensitivity to balance between precision and scalability. However, finer sensitivity does not necessar- ily lead to more precise results but may reduce scalability. Recently, a number of approaches have been proposed to finely tune the sensitivity of different program parts. However, these approaches are usually de- signed for specific program analyses, and their abstraction adjustments are coarse-grained as they directly drop sensitivity elements.

In this paper, we propose a new technique, 4DM, to tune abstractions for program analyses in Datalog. 4DM merges values in a domain, allowing fine-grained sensitivity tuning. 4DM uses a data-driven algorithm for automatically learning a merging strategy for a library from a training set of programs. Unlike existing approaches that rely on the properties of a certain analysis, our learning algorithm works for a wide range of Datalog analyses. We have evaluated our approach on a points-to analysis and a liveness analysis, on the DaCapo benchmark suite. Our evaluation results suggest that our technique achieves a significant speedup and negligible precision loss, reaching a good balance.

Sun 17 Oct

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

09:00 - 10:20
Session 1ASAS at Zurich B +8h
Chair(s): Cezara Drăgoi Inria / ENS / Informal Systems
09:00
15m
Talk
Accelerating Program Analyses in Datalog by Merging Library FactsVirtual
SAS
Yifan Chen Peking University, Chenyang Yang , Xin Zhang Peking University, Yingfei Xiong Peking University, Hao Tang Peking University, Xiaoyin Wang University of Texas at San Antonio, Lu Zhang Peking University
09:15
15m
Talk
Exploiting Verified Neural Networks via Floating Point Numerical ErrorVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard
Pre-print
09:30
15m
Talk
Verifying Low-dimensional Input Neural Networks via Input QuantizationVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology
Pre-print
09:45
15m
Talk
A Multi-Language Static Analysis of Python Programs with Native C ExtensionsVirtual
SAS
Raphaël Monat Sorbonne Université — LIP6, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Pre-print Media Attached
10:00
20m
Live Q&A
Session 1A Discussion, Questions and Answers Virtual
SAS

17:00 - 18:20
Session 1ASAS at Zurich B
Chair(s): Kedar Namjoshi Nokia Bell Labs
17:00
15m
Talk
Accelerating Program Analyses in Datalog by Merging Library FactsVirtual
SAS
Yifan Chen Peking University, Chenyang Yang , Xin Zhang Peking University, Yingfei Xiong Peking University, Hao Tang Peking University, Xiaoyin Wang University of Texas at San Antonio, Lu Zhang Peking University
17:15
15m
Talk
Exploiting Verified Neural Networks via Floating Point Numerical ErrorVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard
Pre-print
17:30
15m
Talk
Verifying Low-dimensional Input Neural Networks via Input QuantizationVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology
Pre-print
17:45
15m
Talk
A Multi-Language Static Analysis of Python Programs with Native C ExtensionsVirtual
SAS
Raphaël Monat Sorbonne Université — LIP6, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Pre-print Media Attached
18:00
20m
Live Q&A
Session 1A Discussion, Questions and Answers Virtual
SAS