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

• Type: Conference
• Year: 2009
• Where: PLDI
• Authors: Satish Chandra, Stephen J. Fink, Manu Sridharan
• Keywords: Graph Construction, PLDI 2009, Programming Languages, Symbolic Analysis, Weakest Preconditions