Humenberger, A., Amrollahi, D., Bjørner, N., & Kovács, L. (2022). Algebra-Based Reasoning for Loop Synthesis. Formal Aspects of Computing, 34(1), 4:31. https://doi.org/10.1145/3527458
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Journal:
Formal Aspects of Computing
-
ISSN:
0934-5043
-
Date (published):
1-Apr-2022
-
Number of Pages:
31
-
Publisher:
ASSOC COMPUTING MACHINERY
-
Peer reviewed:
Yes
-
Keywords:
linear recurrences; loop invariants; Program synthesis; SMT solving; symbolic computation
en
Abstract:
Provably correct software is one of the key challenges of our software-driven society. Program synthesis - the task of constructing a program satisfying a given specification - is one strategy for achieving this. The result of this task is then a program that is correct by design. As in the domain of program verification, handling loops is one of the main ingredients to a successful synthesis procedure.We present an algorithm for synthesizing loops satisfying a given polynomial loop invariant. The class of loops we are considering can be modeled by a system of algebraic recurrence equations with constant coefficients, thus encoding program loops with affine operations among program variables. 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 toward synthesizing loops satisfying a given polynomial loop invariant - program verification - as well as generating number sequences from algebraic relations. To understand viability of the methodology and heuristics for synthesizing loops, we implement and evaluate the method using the Absynth tool.
en
Project title:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission) Distribution Recovery for Invariant Generation of Probabilistic Programs: ICT19-018 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)