Abstraction refinement guided by a learnt probabilistic model

DOI10.1145/2837614.2837663zbMATH Open1347.68084arXiv1511.01874OpenAlexW2264244749MaRDI QIDQ2828290FDOQ2828290

Authors: Radu Grigore, Hongseok Yang 

Publication date: 24 October 2016

Published in: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Abstract: The core challenge in designing an effective static program analysis is to find a good program abstraction -- one that retains only details relevant to a given query. In this paper, we present a new approach for automatically finding such an abstraction. Our approach uses a pessimistic strategy, which can optionally use guidance from a probabilistic model. Our approach applies to parametric static analyses implemented in Datalog, and is based on counterexample-guided abstraction refinement. For each untried abstraction, our probabilistic model provides a probability of success, while the size of the abstraction provides an estimate of its cost in terms of analysis time. Combining these two metrics, probability and cost, our refinement algorithm picks an optimal abstraction. Our probabilistic model is a variant of the Erdos-Renyi random graph model, and it is tunable by what we call hyperparameters. We present a method to learn good values for these hyperparameters, by observing past runs of the analysis on an existing codebase. We evaluate our approach on an object sensitive pointer analysis for Java programs, with two client analyses (PolySite and Downcast).

Full work available at URL: https://arxiv.org/abs/1511.01874

Recommendations

• Learning minimal abstractions
• A Systematic Approach to Probabilistic Pointer Analysis
• Computer Aided Verification
• A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement
• Probabilistic abstract interpretation

zbMATH Keywords

probabilityhypergraphDatalog

Mathematics Subject Classification ID

Applications of graph theory (05C90) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cited In (12)

• Learning minimal abstractions
• Accelerating program analyses in Datalog by merging library facts
• Learning a static analyzer from data
• Abstraction-Refinement for Hierarchical Probabilistic Models
• Learning analysis strategies for Octagon and context sensitivity from labeled data generated by static analyses
• Learning a variable-clustering strategy for Octagon from labeled data generated by a static analysis
• Improving dynamic code analysis by code abstraction
• Learning a Strategy for Choosing Widening Thresholds from a Large Codebase
• Rethinking static analysis by combining discrete and continuous reasoning
• Bias-variance tradeoffs in program analysis
• Computer Aided Verification
• Fast numerical program analysis with reinforcement learning

This page was built for publication: Abstraction refinement guided by a learnt probabilistic model

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2828290)