  Practical adoption of static analysis often requires trading precision for
performance. This paper focuses on improving the memory efficiency of abstract
interpretation without sacrificing precision or time efficiency.
Computationally, abstract interpretation reduces the problem of inferring
program invariants to computing a fixpoint of a set of equations. This paper
presents a method to minimize the memory footprint in Bourdoncle's iteration
strategy, a widely-used technique for fixpoint computation. Our technique is
agnostic to the abstract domain used. We prove that our technique is optimal
(i.e., it results in minimum memory footprint) for Bourdoncle's iteration
strategy while computing the same result. We evaluate the efficacy of our
technique by implementing it in a tool called MIKOS, which extends the
state-of-the-art abstract interpreter IKOS. When verifying user-provided
assertions, MIKOS shows a decrease in peak-memory usage to 4.07% (24.57x) on
average compared to IKOS. When performing interprocedural buffer-overflow
analysis, MIKOS shows a decrease in peak-memory usage to 43.7% (2.29x) on
average compared to IKOS.
