SLR: Path sensitive analysis using infeasible path detection and syntactic language refinement.Gogul Balakrishnan , Sriram Sankaranarayanan , Franjo Ivancic, Ou Wei and Aarti Gupta |
|
We present a technique for detecting semantically infeasible paths
in programs using abstract interpretation. Our technique uses a
sequence of path-insensitive forward and backward runs of an
abstract interpreter to infer paths in the CFG that cannot
be exercised in concrete executions of the program.
We then present a syntactic language refinement (SLR) technique that automatically excludes semantically infeasible paths from the program during the static analysis. This allows us to iteratively prove more properties. Specifically, our technique simulates the effect of a path-sensitive analysis by performing syntactic language refinement over an underlying path-insensitive static analyzer. Finally, we present experimental results to quantify the impact of our technique on an abstract interpreter for C programs.
|
| Static Analysis Symposium (SAS 2008), Vol. 5079 of Lecture Notes in Computer Science, pp. 238-254, Springer-Verlag. |
| Copyright (C) Springer-Verlag. Copy has been made available online for personal use only. Do not redistribute without permission. |