A symbolic analysis framework for static analysis of imperative programming languages
Saved in:
| Title: | A symbolic analysis framework for static analysis of imperative programming languages |
|---|---|
| Authors: | Burgstaller, Bernd1 bburg@cs.yonsei.ac.kr, Scholz, Bernhard2 scholz@it.usyd.edu.au, Blieberger, Johann3 blieb@auto.tuwien.ac.at |
| Source: | Journal of Systems & Software. Jun2012, Vol. 85 Issue 6, p1418-1439. 22p. |
| Subjects: | Symbolic computation, Imperative programming, Programming languages, Computer software, Homomorphisms, Compactification (Mathematics) |
| Abstract: | Abstract: We present a generic symbolic analysis framework for imperative programming languages. Our framework is capable of computing all valid variable bindings of a program at given program points. This information is invaluable for domain-specific static program analyses such as memory leak detection, program parallelization, and the detection of superfluous bound checks, variable aliases and task deadlocks. We employ path expression algebra to model the control flow information of programs. A homomorphism maps path expressions into the symbolic domain. At the center of the symbolic domain is a compact algebraic structure called supercontext. A supercontext contains the complete control and data flow analysis information valid at a given program point. Our approach to compute supercontexts is based purely on algebra and is fully automated. This novel representation of program semantics closes the gap between program analysis and computer algebra systems, which makes supercontexts an ideal symbolic intermediate representation for all domain-specific static program analyses. Our approach is more general than existing methods because it can derive solutions for arbitrary (even intra-loop and nested loop) nodes of reducible and irreducible control flow graphs. We prove the correctness of our symbolic analysis method. Our experimental results show that the problem sizes arising from real-world applications such as the SPEC95 benchmark suite are tractable for our symbolic analysis framework. [Copyright &y& Elsevier] |
| Copyright of Journal of Systems & Software is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 74095444 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: A symbolic analysis framework for static analysis of imperative programming languages – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Burgstaller%2C+Bernd%22">Burgstaller, Bernd</searchLink><relatesTo>1</relatesTo><i> bburg@cs.yonsei.ac.kr</i><br /><searchLink fieldCode="AR" term="%22Scholz%2C+Bernhard%22">Scholz, Bernhard</searchLink><relatesTo>2</relatesTo><i> scholz@it.usyd.edu.au</i><br /><searchLink fieldCode="AR" term="%22Blieberger%2C+Johann%22">Blieberger, Johann</searchLink><relatesTo>3</relatesTo><i> blieb@auto.tuwien.ac.at</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Systems+%26+Software%22">Journal of Systems & Software</searchLink>. Jun2012, Vol. 85 Issue 6, p1418-1439. 22p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Symbolic+computation%22">Symbolic computation</searchLink><br /><searchLink fieldCode="DE" term="%22Imperative+programming%22">Imperative programming</searchLink><br /><searchLink fieldCode="DE" term="%22Programming+languages%22">Programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software%22">Computer software</searchLink><br /><searchLink fieldCode="DE" term="%22Homomorphisms%22">Homomorphisms</searchLink><br /><searchLink fieldCode="DE" term="%22Compactification+%28Mathematics%29%22">Compactification (Mathematics)</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: Abstract: We present a generic symbolic analysis framework for imperative programming languages. Our framework is capable of computing all valid variable bindings of a program at given program points. This information is invaluable for domain-specific static program analyses such as memory leak detection, program parallelization, and the detection of superfluous bound checks, variable aliases and task deadlocks. We employ path expression algebra to model the control flow information of programs. A homomorphism maps path expressions into the symbolic domain. At the center of the symbolic domain is a compact algebraic structure called supercontext. A supercontext contains the complete control and data flow analysis information valid at a given program point. Our approach to compute supercontexts is based purely on algebra and is fully automated. This novel representation of program semantics closes the gap between program analysis and computer algebra systems, which makes supercontexts an ideal symbolic intermediate representation for all domain-specific static program analyses. Our approach is more general than existing methods because it can derive solutions for arbitrary (even intra-loop and nested loop) nodes of reducible and irreducible control flow graphs. We prove the correctness of our symbolic analysis method. Our experimental results show that the problem sizes arising from real-world applications such as the SPEC95 benchmark suite are tractable for our symbolic analysis framework. [Copyright &y& Elsevier] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Journal of Systems & Software is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=74095444 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1016/j.jss.2011.11.1039 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 22 StartPage: 1418 Subjects: – SubjectFull: Symbolic computation Type: general – SubjectFull: Imperative programming Type: general – SubjectFull: Programming languages Type: general – SubjectFull: Computer software Type: general – SubjectFull: Homomorphisms Type: general – SubjectFull: Compactification (Mathematics) Type: general Titles: – TitleFull: A symbolic analysis framework for static analysis of imperative programming languages Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Burgstaller, Bernd – PersonEntity: Name: NameFull: Scholz, Bernhard – PersonEntity: Name: NameFull: Blieberger, Johann IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 06 Text: Jun2012 Type: published Y: 2012 Identifiers: – Type: issn-print Value: 01641212 Numbering: – Type: volume Value: 85 – Type: issue Value: 6 Titles: – TitleFull: Journal of Systems & Software Type: main |
| ResultId | 1 |
