From Affine to Polynomial: Synthesizing Loops with Branches via Algebraic Geometry

Erdenebayar Bayarmagnai, Fatemeh Mohammadi, Rémi Prébet

Ensuring software correctness remains a fundamental challenge in formal program verification. One promising approach relies on finding polynomial invariants for loops. Polynomial i…