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
DOIs
Publication statusPublished - 2006
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

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Symbolic analysis of imperative programming languages'. Together they form a unique fingerprint.

  • 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. https://doi.org/10.1007/11860990_12