用全程序归纳验证数组操作程序
软件工程
2020-02-25 v1 编程语言
摘要
我们提出一种全程序归纳技术，用于证明操作参数化大小N的数组的程序之（一类）量化及无量词性质。我们的技术不对单个循环进行归纳，而是通过程序参数N直接对整个程序（可能包含多个循环）进行归纳。显著的是，这不需要生成或使用循环特定的不变量。我们开发了原型工具Vajra以评估该技术的效能。我们在一组数组操作基准上展示了Vajra相对于若干最先进工具的性能。
引用
@article{arxiv.2002.09857,
title = {Verifying Array Manipulating Programs with Full-Program Induction},
author = {Supratik Chakraborty and Ashutosh Gupta and Divyesh Unadkat},
journal= {arXiv preprint arXiv:2002.09857},
year = {2020}
}