Abstraction refinement guided by a learnt probabilistic model

DOI10.1145/2837614.2837663MaRDI QIDQ2828290zbMATH OpenOpenAlexFDO

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)

Full work available at URL https://arxiv.org/abs/1511.01874, https://kar.kent.ac.uk/54057/1/1511.01874v2.pdf

zbMATH Keywords

Dataloghypergraphprobability

Mathematics Subject Classification ID

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

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).

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

Cited in

(12)

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

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)