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.
翻译:正确无误的软件是软件驱动社会的主要挑战之一。 虽然正式的核查可以确定特定程序的正确性, 程序合成的结果是一个构建正确的程序。 在本文中, 在用环状分析程序时, 我们浏览了两种方案的结果。 我们所考虑的循环类别可以通过一个具有常数的线性重复复现方程式系统( 称为C- 无限复现)来模拟。 我们首先描述一种算法方法, 用于合成非确定性数字单路径环中所有多数值平等的变量。 通过逆向工程合成, 我们然后描述一个合成程序循环的自动方法, 满足了一组给定的多数值圈变量。 我们的结果可以用来证明程序的部分正确性, 编译器优化, 并生成代数关系中的序列。 这是在 VMCAI 2021 上邀请出版的预印本 。