<p>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 <InlineEquation ID="IEq1"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10703_2025_471_Article_IEq1.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="52" /> </InlineMediaObject> <EquationSource Format="TEX">$\textsc {Mikos}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="normal">M</mi> <mstyle mathsize="0.6em"> <mi mathvariant="normal">I</mi> <mi mathvariant="normal">K</mi> <mi mathvariant="normal">O</mi> <mi mathvariant="normal">S</mi> </mstyle> </mrow> </math></EquationSource> </InlineEquation>, which extends the state-of-the-art abstract interpreter <InlineEquation ID="IEq2"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10703_2025_471_Article_IEq2.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="42" /> </InlineMediaObject> <EquationSource Format="TEX">$\text {IKOS}$</EquationSource> <EquationSource Format="MATHML"><math> <mtext>IKOS</mtext> </math></EquationSource> </InlineEquation>. On average <InlineEquation ID="IEq3"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10703_2025_471_Article_IEq3.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="52" /> </InlineMediaObject> <EquationSource Format="TEX">$\textsc {Mikos}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="normal">M</mi> <mstyle mathsize="0.6em"> <mi mathvariant="normal">I</mi> <mi mathvariant="normal">K</mi> <mi mathvariant="normal">O</mi> <mi mathvariant="normal">S</mi> </mstyle> </mrow> </math></EquationSource> </InlineEquation> demonstrated a <InlineEquation ID="IEq4"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10703_2025_471_Article_IEq4.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="54" /> </InlineMediaObject> <EquationSource Format="TEX">$24.57\times $</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mn>24.57</mn> <mo>×</mo> </mrow> </math></EquationSource> </InlineEquation> and <InlineEquation ID="IEq5"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10703_2025_471_Article_IEq5.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="46" /> </InlineMediaObject> <EquationSource Format="TEX">$2.29\times $</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mn>2.29</mn> <mo>×</mo> </mrow> </math></EquationSource> </InlineEquation> reduction in peak-memory usage compared to <InlineEquation ID="IEq6"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10703_2025_471_Article_IEq6.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="42" /> </InlineMediaObject> <EquationSource Format="TEX">$\text {IKOS}$</EquationSource> <EquationSource Format="MATHML"><math> <mtext>IKOS</mtext> </math></EquationSource> </InlineEquation> when verifying user-provided assertions and performing interprocedural buffer-overflow analysis, respectively.</p>

Memory-efficient fixpoint computation

期刊论文
出版模式：

开放获取
发表日期：

2025年4月10日

查看全文

Sung Kook Kim,
Arnaud J. Venet,
Aditya V. Thakur

摘要

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 $\textsc {Mikos}$ $M I K O S$ , which extends the state-of-the-art abstract interpreter $\text {IKOS}$ $IKOS$ . On average $\textsc {Mikos}$ $M I K O S$ demonstrated a $24.57\times $ $24.57 \times$ and $2.29\times $ $2.29 \times$ reduction in peak-memory usage compared to $\text {IKOS}$ $IKOS$ when verifying user-provided assertions and performing interprocedural buffer-overflow analysis, respectively.