# Cut costly functions in inter-procedural abstract interpretation

I am performing some inter-procedural abstract interpretation to capture certain program properties. Following the standard way, what I am doing is to maintain a work list of to-be-analyzed functions, and pick one from the work list to perform intra-procedural analysis until the work list is empty.

Currently, I observed that the intra-procedural analysis of certain functions would not terminate. Basically, it is just taking too much memory and become too slow to reason for even one more statement.

Of course, I can optimize my code base and improve the memory efficiency, but fundamentally that shouldn't help too much.

Now I am seeking for some strategies to bypass such obstacle. Intuitively, what I can do is to cut a intra-procedural analysis off whenever the memory usage grows too high, return a Top as the return value, and switch to the next function in my work list for analysis.

This seems very naturally, and should be sound as well! However, after some quick review of some abstract interpretation work, I don't see any related work performing such cut off.

So here is my question:

1. What is the standard approach in abstract interpretation if a intra-procedural analysis becomes too costly to finish?

2. I assume the cut off and return Top approach is sound. Then why shouldn't I find any related literature employing such approach? Is it too ad-hoc and naive?

• Could you please shed more lights on the counter-example guided refinement method? I never heard of such approaches. Thank you! – lllllllllllll May 6 '17 at 16:16
• Of course, when I said a new input is not a subset of the already-recorded input in the procedural summary. I assume the flow functions of my analysis are all monotonic. – lllllllllllll May 6 '17 at 16:21