Measuring Enforcement Windows with Symbolic Trace Interpretation: What Well-Behaved Programs Say
ISSTA 2012: International Symposium on Software Testing and Analysis
Extended Version: Technical Report CU-CS-1093-12


A static analysis design is sufficient if it can prove the property of interest with an acceptable number of false alarms. Ultimately, the only way to confirm that an analysis design is sufficient is to implement it and run it on real-world programs. If the evaluation shows that the design is insufficient, the designer must return to the drawing board and repeat the process—wasting expensive implementation effort over and over again. In this paper, we make the observation that there is a minimal range of code needed to prove a property of interest under an ideal static analysis; we call such a range of code a validation scope. Armed with this observation, we create a dynamic measurement framework that quantifies validation scopes and thus enables designers to rule out insufficient designs at lower cost. A novel attribute of our framework is the ability to model aspects of static reasoning using dynamic execution measurements. To evaluate the flexibility of our framework, we instantiate it on an example property—null dereference errors—and measure validation scopes on real-world programs. We use a broad range of metrics that capture the difficulty of analyzing programs along varying dimensions. We also examine how validation scopes evolve as developers fix null dereference errors and as code matures. We find that bug fixes shorten validation scopes, that longer validation scopes are more likely to be buggy, and that overall validation scopes are remarkably stable as programs evolve.


@string{ISSTA = "International Symposium on Software Testing and Analysis (ISSTA)"}
  author = {Devin Coughlin and Bor-Yuh Evan Chang and Amer Diwan and Jeremy G. Siek},
  title = {Measuring Enforcement Windows with Symbolic Trace Interpretation: What Well-Behaved Programs Say},
  booktitle = ISSTA,
  year = {2012},
  pages = {276-286},