When analyzing programs, large libraries pose significant challenges to static points-to analysis. A popular solution is to have a human analyst provide points-to specifications that summarize relevant behaviors of library code, which can substantially improve precision and handle missing code such as native code. We propose Atlas, a tool that automatically infers points-to specifications. Atlas synthesizes unit tests that exercise the library code, and then infers points-to specifications based on observations from these executions. Atlas automatically infers specifications for the Java standard library, and produces better results for a client static information flow analysis on a benchmark of 46 Android apps compared to using existing handwritten specifications.
Fri 22 JunDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:40 | |||
14:00 25mTalk | 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 25mTalk | 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 25mTalk | A Data-Driven CHC Solver PLDI Research Papers Media Attached | ||
15:15 25mTalk | User-Guided Program Reasoning using Bayesian Inference PLDI Research Papers Mukund Raghothaman University of Pennsylvania, Sulekha Kulkarni Georgia Tech, Kihong Heo University of Pennsylvania, USA, Mayur Naik University of Pennsylvania Media Attached |