Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
复制标题
DOI：
10.1007/978-3-030-88806-0_20
复制
发表时间：
2021-08
期刊：
影响因子：
--
通讯作者：
Takumi Shimoda;N. Kobayashi;K. Sakayori;Ryosuke Sato
中科院分区：
文献类型：
--
作者：
Takumi Shimoda;N. Kobayashi;K. Sakayori;Ryosuke Sato
尽管最近的自动化程序验证的进步，递归数据结构的推理仍然是验证工具及其后端，如SMT和CHC求解器的挑战。为了解决这个问题，我们引入了符号自动机关系（SAR）的概念，它结合了符号自动机和自动关系，并继承了它们的良好性质，如布尔运算下的闭包。我们认为SAR的可满足性问题，并表明，它是不可判定的一般，但我们可以构建一个健全的（但不完整）和自动满足性检查减少CHC解决。我们讨论了SMT和CHC解决数据结构的应用，并通过实验表明我们的方法的有效性。
Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of symbolic automatic relations (SARs), which combines symbolic automata and automatic relations, and inherits their good properties such as the closure under Boolean operations. We consider the satisfiability problem for SARs, and show that it is undecidable in general, but that we can construct a sound (but incomplete) and automated satisfiability checker by a reduction to CHC solving. We discuss applications to SMT and CHC solving on data structures, and show the effectiveness of our approach through experiments.