SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement

Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivančić, Ou Wei, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

25 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 15th International Symposium, SAS 2008, Proceedings
Pages238-254
Number of pages17
DOIs
StatePublished - Aug 13 2008
Externally publishedYes
Event15th International Static Analysis Symposium, SAS 2008 - Valencia, Spain
Duration: Jul 16 2008Jul 18 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5079 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other15th International Static Analysis Symposium, SAS 2008
CountrySpain
CityValencia
Period7/16/087/18/08

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement'. Together they form a unique fingerprint.

  • Cite this

    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 Static Analysis - 15th International Symposium, SAS 2008, Proceedings (pp. 238-254). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5079 LNCS). https://doi.org/10.1007/978-3-540-69166-2_16