Andrea Flexeder, Michael Petter and Helmut Seidl. Interprocedurally Analysing Linear Inequalities. 18th Nordic Workshop on Programming Theory, Reykjavik, Iceland, 2006.

We present an abstraction of the effect of procedures through convex sets of transition matrices. Conditional branching is handled by postponing the conditional evaluation after the procedure call. In order to obtain an effective analysis convex sets are represented by polyhedra. For an efficient implementation we approximate polyhedra by means of simplices.

Download: PDF Reference: Bibtex