Measuring enforcement windows with symbolic trace interpretation: what well-behaved programs say

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

• Type: Journal
• Year: 2012
• Where: ISSTA
• Authors: Devin Coughlin, Bor-Yuh Evan Chang, Amer Diwan, Jeremy G. Siek
• Keywords: Dynamic Measurement, ISSTA 2012, Measurement Framework, Software Engineering, Symbolic Execution