基于代数的循环及其不变式合成（特邀论文）
计算机科学中的逻辑
2021-03-08 v1
摘要
可证明正确的软件是我们这个由软件驱动的社会中的关键挑战之一。形式化验证确立给定程序的正确性，而程序合成的结果是构造上即正确的程序。在本文中，我们概述了在分析带循环程序时针对这两种情形的一些结果。我们考虑的循环类可由常系数线性递推方程组（称为C-finite递推）建模。我们首先描述一种算法方法，用于合成此类非确定性数值单路径循环的所有多项式等式不变式。然后通过逆向工程不变式合成，我们描述了一种自动化方法，用于合成满足给定多项式循环不变式集的程序循环。我们的结果在程序部分正确性证明、编译器优化以及从代数关系生成数列方面具有应用。这是一篇应邀在VMCAI 2021发表的预印本。
引用
@article{arxiv.2103.03599,
title = {Algebra-based Synthesis of Loops and their Invariants (Invited Paper)},
author = {Andreas Humenberger and Laura Kovacs},
journal= {arXiv preprint arXiv:2103.03599},
year = {2021}
}