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 Jun Times are displayed in time zone: Eastern Time (US & Canada) change
14:00 - 15:40: Program AnalysisPLDI Research Papers at Grand Ballroom CD Chair(s): Isil DilligUT Austin | |||
14:00 - 14:25 Talk | Active Learning of Points-To Specifications PLDI Research Papers Osbert BastaniStanford University, Rahul SharmaMicrosoft Research, Alex AikenStanford University, Percy LiangStanford University Media Attached | ||
14:25 - 14:50 Talk | Pinpoint: Fast and Precise Sparse Value Flow Analysis for Million Lines of Code PLDI Research Papers Qingkai ShiHong Kong University of Science and Technology, China, Xiao XiaoSourceBrella Inc., Rongxin WuDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Jinguo ZhouSourcebrella Inc., Gang Fan, Charles Zhang Media Attached | ||
14:50 - 15:15 Talk | A Data-Driven CHC Solver PLDI Research Papers Media Attached | ||
15:15 - 15:40 Talk | User-Guided Program Reasoning using Bayesian Inference PLDI Research Papers Mukund RaghotamanUniversity of Pennsylvania, Sulekha KulkarniGeorgia Tech, Kihong HeoUniversity of Pennsylvania, USA, Mayur NaikUniversity of Pennsylvania Media Attached |