### 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 language | English |
---|---|

Title of host publication | Modular Programming Languages - 7th Joint Modular Languages Conference, JMLC 2006 Proceedings |

Publisher | Springer Verlag |

Pages | 172-194 |

Number of pages | 23 |

ISBN (Print) | 3540409270, 9783540409274 |

Publication status | Published - 2006 Jan 1 |

Event | 7th Joint Modular Languages Conference, JMLC 2006 - Oxford, United Kingdom Duration: 2006 Sep 13 → 2006 Sep 15 |

### Publication series

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

Volume | 4228 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 7th Joint Modular Languages Conference, JMLC 2006 |
---|---|

Country | United Kingdom |

City | Oxford |

Period | 06/9/13 → 06/9/15 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)

### Cite this

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

}

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

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 -