Analyzing Generalization in Program Analysis

In this content, we explore the concept of generalization in program analysis, focusing on how increased precision can lead to worse results due to unbounded behaviors. Discussions revolve around the need to generalize observations, model the generalization process using the Probably Approximately Correct (PAC) model, and the role of interpolants as classifiers. The empirical study of optimizations in programming tools is also discussed, emphasizing the importance of understanding behaviors in finite time. Through the lenses of abstract interpretation, widening, and interpolants, the content sheds light on the ubiquitous nature of generalization and its impact on program analysis.

• Generalization
• Program Analysis
• Interpolants
• Optimization
• Abstract Interpretation

romo_s Follow

Uploaded on Feb 26, 2025 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

Presentation Transcript

1. Rahul Sharma, Aditya V. Nori, Alex Aiken Stanford MSR India Stanford

2. int i = 1, j = 0; while (i<=5) { j = j+i ; i = i+1; } Invariant inference Intervals ? 1 ? 5 0 ? Octagons ? 1 ? ? ? + 1 Increasing precision Polyhedra ? 5 D. Monniaux and J. L. Guen. Stratified static analysis based on variable dependencies. Electr. Notes Theor. Comput. Sci. 2012

3. A. V. Nori and S. K. Rajamani. An empirical study of optimizations in YOGI. ICSE (1) 2010

4. Increased precision is causing worse results Programs have unbounded behaviors Program analysis Analyze all behaviors Run for a finite time In finite time, observe only finite behaviors Need to generalize

5. Generalization is ubiquitous Abstract interpretation: widening CEGAR: interpolants Parameter tuning of tools Lot of folk knowledge, heuristics,

6. Its all about generalization Learn a function from observations Hope that the function generalizes Work on formalization of generalization

7. Model the generalization process Probably Approximately Correct (PAC) model Explain known observations by this model Use this model to obtain better tools http://politicalcalculations.blogspot.com/2010/02/how-science-is-supposed-to-work.html

8. INTERPOLANTS CLASSIFIERS ++ ++ --- -- + Rahul Sharma, Aditya V. Nori, Alex Aiken: Interpolants as Classifiers. CAV 2012

9. c +++ ++ --- -- Assume an arbitrary but fixed distribution Given ? (iid) samples from Each sample is example ?? with a label?? (+/-)

10. +++ ++ --- -- Empirical error of a hypothesis ?( ) =1 ? ?? ?? ?

11. c +++ ++ --- -- Empirical risk minimization (ERM) Given a set ? of possible hypotheses (precision) Select ? that minimizes empirical error

12. Generalization error: for a new sample (?,?) ?( ) = Pr[ ? ?] Relate generalization error to empirical error and precision

13. Capture precision by VC dimension (VC-d) Higher precision -> More possible hypotheses ?? ? = ? + +- + For any arbitrary labeling H + +- ? 2,? 5, +

14. + + + - + - + - + - - - + + + + + - + - - - - - + - + - + - + -

15. Precision is low Underfitting Y X Precision is high Overfitting Good fit

16. Generalization error is bounded by sum of Bias: Empirical error of best available hypothesis Variance: O(VC-d) Generalization error Variance Bias Possible hypotheses Increase precision

17. Invariant inference int i = 1, j = 0; while (i<=5) { j = j+i ; i = i+1; } Intervals 2? Octagons O(?????) Polyhedra

18. What goes wrong with excess precision? int i = 1, j = 0; while (i<=5) { j = j+i ; i = i+1; } Fit polyhedra to program behaviors Transfer functions, join, widening Intervals: 1 ? 5 0 ? Polyhedra: ? 5 Too many polyhedra, make a wrong choice

19. J. Henry, D. Monniaux, and M. Moy. Pagai: A path sensitive static analyser. Electr. Notes Theor. Comput. Sci. 2012.

20. A. V. Nori and S. K. Rajamani. An empirical study of optimizations in YOGI. ICSE (1) 2010

21. Parameter tuning of program analyses ???? Train Benchmark Set (2490 verification tasks) Tuned ????, test length =500, Overfitting? Generalization on new tasks? P. Godefroid, A. V. Nori, S. K. Rajamani, and S. Tetali. Compositional may-must program analysis: unleashing the power of alternation. POPL 2010.

22. How to set the test length in Yogi Benchmark Set (2490 verification tasks) ????? ????50 Train Training Set (1743) ????50 ????? Test Test Set (747) ?????

23. Performance on test set of tuned ?????s 350 500

24. On 2106 new verification tasks 40% performance improvement! Yogi in production suffers from overfitting

25. Keep separate training and test sets Design of the tools governed by training set Test set as a check SVCOMP: all benchmarks are public Test tools on some new benchmarks too

26. Suggests incrementally increasing precision Find a sweet spot where generalization error is low R. Jhala and K. L. McMillan. A practical and complete approach to predicate refinement. TACAS 2006.

27. VC-d of TCMs: intervals, octagons, etc. Templates: ?1 ?2 Arrays, separation logic Expressive abstract domains -> higher VC-d VC-d can help choose abstractions

28. No generalization -> no bias-variance tradeoff Certain classes of type inference Abstract interpretation without widening Loop-free and recursion-free programs Verify a particular program (e.g., seL4) Overfit on the one important program

29. A model to understand generalization Bias-Variance tradeoffs These tradeoffs do occur in program analysis Understand these tradeoffs for better tools