Memory-efficient fixpoint computation

DOI10.1007/978-3-030-65474-0_3MaRDI QIDQ2233524zbMATH OpenOpenAlexFDO

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

Publication date 18 October 2021

Full work available at URL https://arxiv.org/abs/2009.05865

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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.

Recommendations

• Abstract fixpoint computations with numerical acceleration methods
• Acceleration of the abstract fixpoint computation in numerical program analysis
• Access analysis-based tight localization of abstract memories
• Computer Aided Verification
• Fixpoint Computation in the Polyhedra Abstract Domain Using Convex and Numerical Analysis Tools

Cites work

• Applications of Path Compression on Balanced Trees
• Automating abstract interpretation
• Fast numerical program analysis with reinforcement learning
• Fast polyhedra abstract domain
• Learning a variable-clustering strategy for Octagon from labeled data generated by a static analysis
• Programming Languages and Systems
• Symbolic optimization with SMT solvers
• Verification, Model Checking, and Abstract Interpretation

Cited in

(5)

• scientific article; zbMATH DE number 7119801 (Why is no real title available?)
• Mapping Computation with No Memory
• Memory-tight reductions
• scientific article; zbMATH DE number 4179292 (Why is no real title available?)
• Access analysis-based tight localization of abstract memories

This page was built for publication: Memory-efficient fixpoint computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233524)