Fri 22 Jun 2018 14:25 - 14:50 at Grand Ballroom CD - Program Analysis Chair(s): Isil Dillig

When dealing with millions of lines of code, we still cannot have the cake and eat it: sparse value-flow analysis is powerful in checking source-sink problems, but existing work cannot escape from the “pointer trap” – a precise points-to analysis limits its scalability and an imprecise one seriously undermines its precision. We present Pinpoint, a holistic approach that decomposes the cost of high-precision points-to analysis by precisely discovering local data dependence and delaying the expensive inter-procedural analysis through memorization. Such memorization enables the on-demand slicing of only the necessary inter-procedural data dependence and path feasibility queries, which are then solved by a costly SMT solver. Experiments show that Pinpoint can check programs such as MySQL (around 2 million lines of code) within 1.5 hours. The overall false positive rate is also very low (14.3% - 23.6%). Pinpoint has discovered over forty real bugs in mature and extensively checked open source systems. And the implementation of Pinpoint and all experimental results are freely available.

Fri 22 Jun

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

14:00 - 15:40
Program AnalysisPLDI Research Papers at Grand Ballroom CD
Chair(s): Isil Dillig UT Austin
14:00
25m
Talk
Active Learning of Points-To Specifications
PLDI Research Papers
Osbert Bastani Stanford University, Rahul Sharma Microsoft Research, Alex Aiken Stanford University, Percy Liang Stanford University
Media Attached
14:25
25m
Talk
Pinpoint: Fast and Precise Sparse Value Flow Analysis for Million Lines of Code
PLDI Research Papers
Qingkai Shi Hong Kong University of Science and Technology, China, Xiao Xiao SourceBrella Inc., Rongxin Wu Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Jinguo Zhou Sourcebrella Inc., Gang Fan , Charles Zhang
Media Attached
14:50
25m
Talk
A Data-Driven CHC Solver
PLDI Research Papers
He Zhu Rutgers University, USA, Stephen Magill , Suresh Jagannathan Purdue University
Media Attached
15:15
25m
Talk
User-Guided Program Reasoning using Bayesian Inference
PLDI Research Papers
Mukund Raghotaman University of Pennsylvania, Sulekha Kulkarni Georgia Tech, Kihong Heo University of Pennsylvania, USA, Mayur Naik University of Pennsylvania
Media Attached