Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
复制标题
通过符号执行用位向量算术证明程序的终止
DOI：
10.1007/978-3-319-41591-8_16
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Thomas Ströder
中科院分区：
文献类型：
--
作者：
Jera Hensel;J. Giesl;Florian Frohn;Thomas Ströder
在早期工作中，我们开发了一种基于符号执行的显式指针算术自动终止分析 C 程序的方法。然而，与许多其他终止技术类似，这种方法假设程序变量的范围是数学整数而不是位向量。这简化了数学推理，但总的来说是不合理的。在本文中，我们扩展了我们的方法以处理固定宽度的位向量整数。因此，我们提出了第一种 C 程序终止分析技术，涵盖了字节精确指针算术和整数位精确建模。我们在自动端接验证器 AProVE 中实施了我们的方法，并通过大量实验评估其功能。
In earlier work, we developed an approach for automated termination analysis of C programs with explicit pointer arithmetic, which is based on symbolic execution. However, similar to many other termination techniques, this approach assumed the program variables to range over mathematical integers instead of bitvectors. This eases mathematical reasoning but is unsound in general. In this paper, we extend our approach in order to handle fixed-width bitvector integers. Thus, we present the first technique for termination analysis of C programs that covers both byte-accurate pointer arithmetic and bit-precise modeling of integers. We implemented our approach in the automated termination prover AProVE and evaluate its power by extensive experiments.