We present an algorithm for synthesizing program loops satisfying a given polynomial loop invariant. The class of loops we consider can be modeled by a system of algebraic recurrence equations with constant coefficients. We turn the task of loop synthesis into a polynomial constraint problem by precisely characterizing the set of all loops satisfying the given invariant. We prove soundness of our approach, as well as its completeness with respect to an a priori fixed upper bound on the number of program variables. Our work has applications towards program verification, as well as generating number sequences from algebraic relations. We implemented our work in the Absynth tool and report on our initial experiments with loop synthesis.
Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors
Key Laboratory of High Confidence Software Technologies (Peking University), Ministry of Education（北京大学计算机学院）；School of Computer Science , Peking University（蚂蚁集团）；Ant Group
Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning
Australian National University（澳大利亚国立大学）；Data61, CSIRO（联邦科学与工业研究组织数据61所）；Chiba University（千叶大学）；University of Tsukuba（筑波大学）；RIKEN AIP（理化学研究所人工智能项目中心）；National Institute of Informatics（国立信息学研究所）；Kyoto University（京都大学）
