Solving and Interpolating Constant Arrays Based on Weak Equivalences
Solving and Interpolating Constant Arrays Based on Weak Equivalences
复制标题
基于弱等价的常量数组求解和插值
DOI：
10.1007/978-3-030-11245-5_14
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
T. Schindler
中科院分区：
文献类型：
--
作者：
J. Hoenicke;T. Schindler
提出了一种新的求解器和插值算法，用于常数阵列的阵列理论。它是基于我们以前的工作弱等价数组。常量数组在每个索引处存储相同的值，这对于初始化内存的程序的模型检查很有用。与使用存储链显式初始化内存不同，使用常量数组可以大大简化查询，从而减少求解和插值时间。我们表明，只有几个新的规则所需的常数阵列，并证明了正确的决策过程和插值过程。我们在我们的插值求解器SMTInterpol中实现了该算法。
We present a new solver and interpolation algorithm for the theory of arrays with constant arrays. It is based on our previous work on weakly equivalent arrays. Constant arrays store the same value at every index, which is useful for model checking of programs with initialised memory. Instead of using a store chain to explicitly initialise the memory, using a constant array can considerably simplify the queries and thus reduce the solving and interpolation time. We show that only a few new rules are required for constant arrays and prove the correctness of the decision procedure and the interpolation procedure. We implemented the algorithm in our interpolating solverSMTInterpol.
登录
查看更多内容
DOI：
--
发表时间：
2013
期刊：
International Conference on Tools and Algorithms for Construction and Analysis of Systems
影响因子：
--
作者：
Jürgen Christ;Jochen Hoenicke;Alexander Nutz
通讯作者：
Alexander Nutz
完整的基于实例化的插值
DOI：
--
发表时间：
2013
期刊：
Journal of automated reasoning
影响因子：
--
作者：
Nishant Totla;Thomas Wies
通讯作者：
Thomas Wies
支持递归程序和浮点运算的 CPAchecker -（竞赛贡献）
DOI：
--
发表时间：
2015
期刊：
International Conference on Tools and Algorithms for Construction and Analysis of Systems
影响因子：
--
作者：
Matthias Dangl;Stefan Löwe;Philipp Wendler
通讯作者：
Philipp Wendler
DOI：
--
发表时间：
2012
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
M. Bodirsky;P. Jonsson;T. Oertzen
通讯作者：
T. Oertzen