Memory-Efficient Fixpoint Computation
summary
A technique interleaves assertion checks with Bourdoncle-style recursive fixpoint iteration to free abstract values early, implemented as MIKOS extends IKOS and applied to 784 SV-COMP and 426 Arch Linux package benchmarks. The algorithm computes optimal deallocation and assertion-evaluation points in almost-linear time, preserves precision, and keeps time similar (geometric speedups 1.3x and 1.08x). Memory falls dramatically: geometric mean 25x improvement (min 1.11x, max 1000x), examples cut 46 GB→56 MB and 64 GB→21 GB.
AI-written summary · about
chapters (5)
- 0:00Introduction
- 0:20Abstract Interpretation
- 10:23Theoretical Results
- 11:00Empirical Results
- 15:28Summary
related talks
23mBeating the Benchmarks: Co-evolving the ISA and Development Tools
01h 04mWe Live in Interesting Times
50mRecent Advances in Floating-point (Static) Analyses
14mOracle-Free Repair Synthesis for Floating-Point Programs
22mModular Optimization-Based Roundoff Error Analysis of Floating-Point Programs
22mFungible Memories for Automated Technology Mapping and Retargeting
57mInvited Talk: Bridging Safety and Performance
42mAdventures in Efficiency and Performance