Interprocedurally Analysing Linear Inequality Relations

13 years 10 months ago

Download www2.in.tum.de

In this paper we present an alternative approach to interprocedurally g linear inequality relations. We propose an abstraction of the effects of procedures through convex sets of transition matrices. In the absence of condiranching, this abstraction can be characterised precisely by means of the least solution of a constraint system. In order to handle conditionals, we introduce auxiliary variables and postpone checking them until after the procedure calls. In order to obtain an effective analysis, we approximate convex sets by means of polyhedra. Since our implementation of function composition uses the frame representation of polyhedra, we rely on the subclass of simplices to obtain an efimplementation. We show that for this abstraction the basic operations can be implemented in polynomial time. First practical experiments indicate that the resulting analysis is quite efﬁcient and provides reasonably precise results.

Helmut Seidl, Andrea Flexeder, Michael Petter

Real-time Traffic