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

29 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 - 2008
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
Country/TerritorySpain
CityValencia
Period7/16/087/18/08

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

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