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 control flow graph 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 a program during static analysis. SLR 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. © 2008 Springer-Verlag.
CITATION STYLE
Balakrishnan, G., Sankaranarayanan, S., Ivančić, F., Wei, O., & Gupta, A. (2008). SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5079 LNCS, pp. 238–254). https://doi.org/10.1007/978-3-540-69166-2_16
Mendeley helps you to discover research relevant for your work.