On Abstraction Refinement for Bayesian Program Analysis
summary
Paper proposes an online abstraction search called BSRefine that performs counterexample-guided refinement on Bayesian program analyses by cutting information channels identified via conditional independence theory, encoding the cut as a partial weighted max‑set problem and solving it with a max‑set solver. Implementations on a Bayesian datarace and Bayesian thread‑escape analysis evaluate on 12 Java benchmarks, reduce false alarms (example reduces three false positives to two), and add little runtime overhead while improving ranking, especially when offline training is suboptimal.
AI-written summary · about
chapters (13)
- 0:00Bayesian program analysis
- 1:30Abstraction selection challenges
- 2:12Example program and data flow
- 3:59Bayesian network transformation
- 5:03Counterexample-guided refinement
- 6:29Conditional independence
- 8:15Information transmission graph
- 9:19Refining abstraction for alarms
- 10:03BestRefine workflow
- 11:04Experimental evaluation
- 12:32Comparison with parameter learning
- 12:53Efficiency and scalability
- 13:14Conclusion
related talks
18mLearning Abstraction Selection for Bayesian Program Analysis
24mFuzzing Guided by Bayesian Program Analysis
13mTowards Compiling Higher-Order Programs to Bayesian Networks
14mSequential Monte Carlo Program Synthesis with Refinement Proposals
31mARENA: Enhancing Abstract Refinement for Neural Network Verification
59mWhat Can Program Analysis Say About Data Bias?
21mScaling Abstraction Refinement for Program Analyses in Datalog Using Graph Neural(…)
01h 03mAn Overview of Probabilistic Programming