基于线性递归分析的组合不变式生成
Compositional Invariant Generation via Linear Recurrence Analysis
摘要：
本文提出了一种自动生成命令式程序数值不变量的新方法。给定一个程序，我们的程序计算一个二进制的输入/输出关系的程序状态过近似的行为的程序。它是组合的，因为它通过将程序分解为多个部分，计算每个部分的抽象含义，然后组合这些含义来运行。我们的方法近似循环行为的基础上，首先近似的循环体的意义，从近似提取递归关系，然后使用封闭的形式来近似循环。我们的实验表明，在验证任务，我们的方法是有竞争力的领先的不变生成和验证工具。
英文摘要：
This paper presents a new method for automatically generating numerical invariants for imperative programs. Given a program, our procedure computes a binary input/output relation on program states which over-approximates the behaviour of the program. It is compositional in the sense that it operates by decomposing the program into parts, computing an abstract meaning of each part, and then composing the meanings. Our method for approximating loop behaviour is based on first approximating the meaning of the loop body, extracting recurrence relations from that approximation, and then using the closed forms to approximate the loop. Our experiments demonstrate that on verification tasks, our method is competitive with leading invariant generation and verification tools.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
