Floating-Point TVPI Abstract Domain for Numerical Program Analysis

Explore a 17-minute video presentation from the PLDI 2024 conference introducing the Two Variables per Inequality Floating-Point (TVPI-FP) domain, a novel abstract domain for analyzing floating-point programs. Learn how this numerical and constraint-based approach overcomes limitations of existing tools by supporting conditional branches, loops, and elementary functions while maintaining efficiency. Discover the key idea of using interval arithmetic in inequalities and how it leads to redesigned operators. Examine the experimental results demonstrating TVPI-FP's superior speed and competitive precision compared to more expressive tools, as well as its broader support for realistic programs with complex structures.