Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings
Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings
复制标题
智能计算机数学 - 第 15 届国际会议，CICM 2022，格鲁吉亚第比利斯，2022 年 9 月 19-23 日，会议记录
DOI：
10.1007/978-3-031-16681-5_14
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Bhayat A
中科院分区：
文献类型：
--
作者：
Bhayat A
我们提出了一种新的方法来自动验证一阶归纳程序的属性捕获的部分正确性的命令式程序循环与分支，整数和数组。我们依赖于跟踪逻辑，一阶逻辑的实例与理论，表示一阶程序语义的量化程序执行时间点。跟踪逻辑中的程序验证被转化为一阶定理证明问题，到目前为止，有效的推理需要引入所谓的跟踪引理来建立归纳性质。在这项工作中，我们扩展跟踪逻辑与通用归纳图式的时间点和循环计数器，减少依赖跟踪引理。循环不变量的推导和证明成为基于叠加的一阶定理证明中的归纳推理步骤。我们在Rapid框架中实现了我们的方法，使用了一阶定理证明器Vampire。我们广泛的实验分析表明，自动归纳验证跟踪逻辑是一个改进，现有的方法相比。
We present a novel approach to automate the verification of first-order inductive program properties capturing the partial correctness of imperative program loops with branching, integers and arrays. We rely on trace logic, an instance of first-order logic with theories, to express first-order program semantics by quantifying over program execution timepoints. Program verification in trace logic is translated into a first-order theorem proving problem where, to date, effective reasoning has required the introduction of so-called trace lemmas to establish inductive properties. In this work, we extend trace logic with generic induction schemata over timepoints and loop counters, reducing reliance on trace lemmas. Inferring and proving loop invariants becomes an inductive inference step within superposition-based first-order theorem proving. We implemented our approach in theRapidframework, using the first-order theorem proverVampire. Our extensive experimental analysis shows that automating inductive verification in trace logic is an improvement compared to existing approaches.