符号自动关系及其在 SMT 与 CHC 求解中的应用
计算机科学中的逻辑
2021-08-24 v1 编程语言
摘要
尽管自动化程序验证近期取得了进展，对递归数据结构的推理仍是验证工具及其后端（如 SMT 和 CHC 求解器）面临的挑战。为应对该挑战，我们引入了符号自动关系（SARs）的概念，它结合了符号自动机与自动关系，并继承了它们在布尔运算下封闭等良好性质。我们考虑 SARs 的可满足性问题，证明其在一般情况下不可判定，但可通过归约到 CHC 求解构造一个可靠（但不完备）的自动化可满足性检查器。我们讨论了在数据结构的 SMT 和 CHC 求解上的应用，并通过实验展示了我们方法的有效性。
引用
@article{arxiv.2108.07642,
title = {Symbolic Automatic Relations and Their Applications to SMT and CHC Solving},
author = {Takumi Shimoda and Naoki Kobayashi and Ken Sakayori and Ryosuke Sato},
journal= {arXiv preprint arXiv:2108.07642},
year = {2021}
}
备注
A shorter version will appear in Proceedings of SAS 2021