Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Guided Static Analysis
| Book Series | Lecture Notes in Computer Science |
| Publisher | Springer Berlin / Heidelberg |
| ISSN | 0302-9743 (Print) 1611-3349 (Online) |
| Volume | Volume 4634/2007 |
| Book | Static Analysis |
| DOI | 10.1007/978-3-540-74061-2 |
| Copyright | 2007 |
| ISBN | 978-3-540-74060-5 |
| DOI | 10.1007/978-3-540-74061-2_22 |
| Pages | 349-365 |
| Subject Collection | Computer Science |
| SpringerLink Date | Wednesday, August 22, 2007 |
| |
|
Denis Gopan1 and Thomas Reps1, 2 
| (1) |
University of Wisconsin, |
Abstract
In static analysis, the semantics of the program is expressed as a set of equations. The equations are solved iteratively
over some abstract domain. If the abstract 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 state-space 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 instantiations of the framework, which improve the precision of widening in (i) loops with multiple phases
and (ii) loops in which the transformation performed on each iteration is chosen non-deterministically.
Supported by ONR under grant N00014-01-1-0796 and by NSF under grants CCF-0540955 and CCF-0524051.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|