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

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

doi:10.1007/978-3-540-69166-2_16

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

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Static Analysis - 15th International Symposium, SAS 2008, Proceedings
Pages	238-254
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-540-69166-2_16
State	Published - 2008
Event	15th International Static Analysis Symposium, SAS 2008 - Valencia, Spain Duration: Jul 16 2008 → Jul 18 2008

Publication series

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

Other

Other	15th International Static Analysis Symposium, SAS 2008
Country/Territory	Spain
City	Valencia
Period	7/16/08 → 7/18/08

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-540-69166-2_16

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

Balakrishnan, Gogul ; Sankaranarayanan, Sriram ; Ivančić, Franjo et al. / SLR : Path-sensitive analysis through infeasible-path detection and syntactic language refinement. Static Analysis - 15th International Symposium, SAS 2008, Proceedings. 2008. pp. 238-254 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9686338694694b46851af098a9d57201,

title = "SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement",

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.",

author = "Gogul Balakrishnan and Sriram Sankaranarayanan and Franjo Ivan{\v c}i{\'c} and Ou Wei and Aarti Gupta",

year = "2008",

doi = "10.1007/978-3-540-69166-2_16",

language = "English (US)",

isbn = "3540691634",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "238--254",

booktitle = "Static Analysis - 15th International Symposium, SAS 2008, Proceedings",

note = "15th International Static Analysis Symposium, SAS 2008 ; Conference date: 16-07-2008 Through 18-07-2008",

}

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

SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement. / Balakrishnan, Gogul; Sankaranarayanan, Sriram; Ivančić, Franjo et al.
Static Analysis - 15th International Symposium, SAS 2008, Proceedings. 2008. p. 238-254 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5079 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - SLR

T2 - 15th International Static Analysis Symposium, SAS 2008

AU - Balakrishnan, Gogul

AU - Sankaranarayanan, Sriram

AU - Ivančić, Franjo

AU - Wei, Ou

AU - Gupta, Aarti

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=48949085922&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=48949085922&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-69166-2_16

DO - 10.1007/978-3-540-69166-2_16

M3 - Conference contribution

AN - SCOPUS:48949085922

SN - 3540691634

SN - 9783540691631

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 238

EP - 254

BT - Static Analysis - 15th International Symposium, SAS 2008, Proceedings

Y2 - 16 July 2008 through 18 July 2008

ER -

Balakrishnan G, Sankaranarayanan S, Ivančić F, Wei O, Gupta A. SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement. In Static Analysis - 15th International Symposium, SAS 2008, Proceedings. 2008. p. 238-254. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-69166-2_16

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

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this