Fast Numerical Program Analysis with Reinforcement Learning
OPEN ACCESS
Loading...
Author / Producer
Date
2018
Publication Type
Conference Paper
ETH Bibliography
yes
OPEN ACCESS
Data
Rights / License
Abstract
We show how to leverage reinforcement learning (RL) in order to speed up static program analysis. The key insight is to establish a correspondence between concepts in RL and those in analysis: a state in RL maps to an abstract program state in analysis, an action maps to an abstract transformer, and at every state, we have a set of sound transformers (actions) that represent different trade-offs between precision and performance. At each iteration, the agent (analysis) uses a policy learned offline by RL to decide on the transformer which minimizes loss of precision at fixpoint while improving analysis performance. Our approach leverages the idea of online decomposition (applicable to popular numerical abstract domains) to define a space of new approximate transformers with varying degrees of precision and performance. Using a suitably designed set of features that capture key properties of abstract program states and available actions, we then apply Q-learning with linear function approximation to compute an optimized context-sensitive policy that chooses transformers during analysis. We implemented our approach for the notoriously expensive Polyhedra domain and evaluated it on a set of Linux device drivers that are expensive to analyze. The results show that our approach can yield massive speedups of up to two orders of magnitude while maintaining precision at fixpoint.
Permanent link
Publication status
published
External links
Book title
Computer Aided Verification
Journal / series
Volume
10981
Pages / Article No.
211 - 229
Publisher
Springer
Event
International Conference on Computer-Aided Verification (CAV)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03893 - Püschel, Markus / Püschel, Markus
03948 - Vechev, Martin / Vechev, Martin
Notes
Funding
163117 - Making Program Analysis Fast (SNF)
Related publications and datasets
Is part of: https://doi.org/10.3929/ethz-b-000445921