We present the abstraction of the effect of procedures
through convex sets of transition matrices.
Handling conditinal branching is
realised by introducing auxilary variables and postponing the conditional evaluation after the
procedure call.
In order to obtain an effective analysis convex sets are
approximated by polyhedrea.
For an efficient implementation we approximate by
means of simplices.
| Example programs | Running time Polyhedron/Simplex | Inequalities at the end of main |
|---|---|---|
| recursive add | 0.234sec / 0.134sec | result2=result1=result=8 y=3 x=5 |
| loop bound | 15.132sec / 0.449sec | i>=0 c-i>=1 |
| example of mine | 2.417sec /0.325sec | x>= 40 x<= 41 |
| interprocedural example1 | 0.168sec / 0.029sec | a=5 i=6 |