Sciweavers

Share
PLDI
2009
ACM

Snugglebug: a powerful approach to weakest preconditions

10 years 6 months ago
Snugglebug: a powerful approach to weakest preconditions
Symbolic analysis shows promise as a foundation for bug-finding, specification inference, verification, and test generation. This paper addresses demand-driven symbolic analysis for object-oriented programs and frameworks. Many such codes comprise large, partial programs with highly dynamic behaviors—polymorphism, reflection, and so on—posing significant scalability challenges for any static analysis. We present an approach based on interprocedural backwards propagation of weakest preconditions. We present several novel techniques to improve the efficiency of such analysis. First, we present directed call graph construction, where call graph construction and symbolic analysis are interleaved. With this technique, call graph construction is guided by constraints discovered during symbolic analysis, obviating the need for exhaustively exploring a large, conservative call graph. Second, we describe generalization, a technique that greatly increases the reusability of procedure ...
Satish Chandra, Stephen J. Fink, Manu Sridharan
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where PLDI
Authors Satish Chandra, Stephen J. Fink, Manu Sridharan
Comments (0)
books