Precise interprocedural analysis through linear algebra

Markus Müller-Olm, Helmut Seidl

Research output: Contribution to journalConference articlepeer-review

63 Scopus citations

Abstract

We apply linear algebra techniques to precise interprocedural dataflow analysis. Specifically, we describe analyses that determine for each program point identities that are valid among the program variables whenever control reaches that program point. Our analyses fully interpret assignment statements with affine expressions on the right hand side while considering other assignments as non-deterministic and ignoring conditions at branches. Under this abstraction, the analysis computes the set of all affine relations and, more generally, all polynomial relations of bounded degree precisely. The running lime of our algorithms is linear in the program size and polynomial in the number of occurring variables. We also show how to deal with affine preconditions and local variables and indicate how to handle parameters and return values of procedures.

Original languageEnglish
Pages (from-to)330-341
Number of pages12
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
Volume31
DOIs
StatePublished - 2004
EventConference Record of POPL 2004 - 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Venice, Italy
Duration: 14 Jan 200416 Jan 2004

Keywords

  • Affine relation
  • Interprocedural analysis
  • Linear algebra
  • Polynomial relation
  • Weakest precondition

Fingerprint

Dive into the research topics of 'Precise interprocedural analysis through linear algebra'. Together they form a unique fingerprint.

Cite this