Guided Static Analysis

In static analysis, the semantics of the program is expressed as a set ions. The equations are solved iteratively over some abstract domain. If ract domain is distributive and satisfies the ascending-chain condition, an iterative technique yields the most precise solution for the equations. However, if the above properties are not satisfied, the solution obtained is typically imprecise. Moreover, due to the properties of widening operators, the precision loss is sensitive to the order in which the state-space is explored. In this paper, we introduce guided static analysis, a framework for controlling the exploration of the state-space of a program. The framework guides the statespace exploration by applying standard static-analysis techniques to a sequence of modified versions of the analyzed program. As such, the framework does not require any modifications to existing analysis techniques, and thus can be easily integrated into existing static-analysis tools. We present two instan...

• Type: Conference
• Year: 2007
• Where: SAS
• Authors: Denis Gopan, Thomas W. Reps
• Keywords: Abstract Domain, Formal Methods, SAS 2007, Set Ions, Static Analysis