基于代数的循环及其不变量的合成（邀请论文）
Algebra-based Synthesis of Loops and their Invariants (Invited Paper)
摘要：
可证明正确的软件是我们软件驱动社会的关键挑战之一。形式化验证确定给定程序的正确性，而程序合成的结果是一个通过构造而正确的程序。在本文中，我们概述了我们的一些结果，这两种情况下，分析程序与循环。我们考虑的循环类可以用一个常系数线性递归方程组来建模，称为C-有限递归。首先，我们描述了一种算法方法，用于合成所有的多项式等式不变量的非确定性数值单路径循环。通过逆向工程不变量合成，我们描述了一种自动化的方法来合成程序循环满足一组给定的多项式循环不变量。我们的结果证明部分正确的程序，编译器优化和生成的代数关系的数列的应用。这是邀请在VMCAI 2021上出版的预印本。
英文摘要：
Provably correct software is one of the key challenges in our softwaredriven society. While formal verification establishes the correctness of a given program, the result of program synthesis is a program which is correct by construction. In this paper we overview some of our results for both of these scenarios when analysing programs with loops. The class of loops we consider can be modelled by a system of linear recurrence equations with constant coefficients, called C-finite recurrences. We first describe an algorithmic approach for synthesising all polynomial equality invariants of such non-deterministic numeric single-path loops. By reverse engineering invariant synthesis, we then describe an automated method for synthesising program loops satisfying a given set of polynomial loop invariants. Our results have applications towards proving partial correctness of programs, compiler optimisation and generating number sequences from algebraic relations. This is a preprint that was invited for publication at VMCAI 2021.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
