用数据驱动方法自动验证含整数数组的程序，提升验证效率与准确性。
Data-driven Verification of Procedural Programs with Integer Arrays
- 基于决策树框架，将数组问题转化为整数向量分类学习。
- 可自动生成带全称量词的循环不变式和过程前后条件，覆盖参数化数组。
- 在多个基准测试中表现优于现有工具，适合形式化验证研究者使用。
我们针对自动验证操作参数化大小整数数组的程序这一问题展开研究，将问题建模为约束霍恩子句求解任务。提出一种新算法，用于合成以全称量化一阶公式表示的循环不变式与过程前置/后置条件，这些公式约束数组元素和程序变量。采用数据驱动方法，扩展了决策树霍恩-ICE框架以处理数组结构。通过将复杂的整数数组向量分类问题简化为更简单的整数向量分类问题，实现高效学习。所得分类器被泛化为全称量化不变式与过程条件。我们已实现该方法，并在大规模基准测试中证明其效率与先进工具相当甚至更优。
原文摘要 · Abstract (English)
We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We propose a new algorithmic method for synthesizing loop invariants and procedure pre/post-conditions represented as universally quantified first-order formulas constraining the array elements and program variables. We adopt a data-driven approach that extends the decision tree Horn-ICE framework to handle arrays. We provide a powerful learning technique based on reducing a complex classification problem of vectors of integer arrays to a simpler classification problem of vectors of integers. The obtained classifier is generalized to get universally quantified invariants and procedure pre/post-conditions. We have implemented our method and shown its efficiency and competitiveness w.r.t. state-of-the-art tools on a significant benchmark.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。