Beyond Affine Loops - A Geometric Approach to Program Synthesis

Explore a novel geometric approach to program synthesis that extends beyond traditional affine loops in this 19-minute conference presentation from SOAP 2025. Learn how researchers from KU Leuven and Inria tackle the fundamental challenge of software correctness verification by developing an algorithm that synthesizes loops with polynomial update maps, guard conditions with inequations, and polynomial invariants of arbitrary form. Discover how algebraic geometry tools are applied to reduce the loop synthesis problem to solving polynomial systems within specified subsets of complex numbers, with practical implementation using SMT solvers. Understand the theoretical foundations and practical implications of this advancement in formal program verification, moving beyond existing methods that only handle affine loops without guard conditions to address more general polynomial invariant synthesis problems.