Symbolic analysis of imperative programming languages

bernd Burgstaller, Bernhard Scliolz, Johann Blieberger

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

6 Citations (Scopus)

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 invaluably for domain-specific static program analyses such as memory leak detection, program parallelisation. 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 homomorpliism 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 und computer algebra systems, which makes supercontexts an ideal 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) 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.

Original languageEnglish
Title of host publicationModular Programming Languages - 7th Joint Modular Languages Conference, JMLC 2006 Proceedings
PublisherSpringer Verlag
Pages172-194
Number of pages23
ISBN (Print)3540409270, 9783540409274
Publication statusPublished - 2006 Jan 1
Event7th Joint Modular Languages Conference, JMLC 2006 - Oxford, United Kingdom
Duration: 2006 Sep 132006 Sep 15

Publication series

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

Other

Other7th Joint Modular Languages Conference, JMLC 2006
CountryUnited Kingdom
CityOxford
Period06/9/1306/9/15

Fingerprint

Symbolic Analysis
Computer programming languages
Algebra
Programming Languages
Data flow analysis
Flow graphs
Leak detection
Flow control
Computer systems
Semantics
Data storage equipment
Valid
Path
Flow Graphs
Program Analysis
Computer algebra system
Deadlock
Information Flow
Flow Control
Real-world Applications

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Burgstaller, B., Scliolz, B., & Blieberger, J. (2006). Symbolic analysis of imperative programming languages. In Modular Programming Languages - 7th Joint Modular Languages Conference, JMLC 2006 Proceedings (pp. 172-194). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4228 LNCS). Springer Verlag.
Burgstaller, bernd ; Scliolz, Bernhard ; Blieberger, Johann. / Symbolic analysis of imperative programming languages. Modular Programming Languages - 7th Joint Modular Languages Conference, JMLC 2006 Proceedings. Springer Verlag, 2006. pp. 172-194 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{098919955e724387857f66ced85436dd,
title = "Symbolic analysis of imperative programming languages",
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 invaluably for domain-specific static program analyses such as memory leak detection, program parallelisation. 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 homomorpliism 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 und computer algebra systems, which makes supercontexts an ideal 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) 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.",
author = "bernd Burgstaller and Bernhard Scliolz and Johann Blieberger",
year = "2006",
month = "1",
day = "1",
language = "English",
isbn = "3540409270",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "172--194",
booktitle = "Modular Programming Languages - 7th Joint Modular Languages Conference, JMLC 2006 Proceedings",
address = "Germany",

}

Burgstaller, B, Scliolz, B & Blieberger, J 2006, Symbolic analysis of imperative programming languages. in Modular Programming Languages - 7th Joint Modular Languages Conference, JMLC 2006 Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4228 LNCS, Springer Verlag, pp. 172-194, 7th Joint Modular Languages Conference, JMLC 2006, Oxford, United Kingdom, 06/9/13.

Symbolic analysis of imperative programming languages. / Burgstaller, bernd; Scliolz, Bernhard; Blieberger, Johann.

Modular Programming Languages - 7th Joint Modular Languages Conference, JMLC 2006 Proceedings. Springer Verlag, 2006. p. 172-194 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4228 LNCS).

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

TY - GEN

T1 - Symbolic analysis of imperative programming languages

AU - Burgstaller, bernd

AU - Scliolz, Bernhard

AU - Blieberger, Johann

PY - 2006/1/1

Y1 - 2006/1/1

N2 - 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 invaluably for domain-specific static program analyses such as memory leak detection, program parallelisation. 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 homomorpliism 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 und computer algebra systems, which makes supercontexts an ideal 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) 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.

AB - 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 invaluably for domain-specific static program analyses such as memory leak detection, program parallelisation. 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 homomorpliism 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 und computer algebra systems, which makes supercontexts an ideal 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) 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.

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

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

M3 - Conference contribution

SN - 3540409270

SN - 9783540409274

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

SP - 172

EP - 194

BT - Modular Programming Languages - 7th Joint Modular Languages Conference, JMLC 2006 Proceedings

PB - Springer Verlag

ER -

Burgstaller B, Scliolz B, Blieberger J. Symbolic analysis of imperative programming languages. In Modular Programming Languages - 7th Joint Modular Languages Conference, JMLC 2006 Proceedings. Springer Verlag. 2006. p. 172-194. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).