通过求解无递归Horn子句的广义插值
计算机科学中的逻辑
2014-12-04 v2
摘要
本文介绍了InterHorn，一个用于无递归Horn子句的求解器。InterHorn的主要应用领域在于解决软件验证中出现的插值问题。我们展示了如何直接通过InterHorn处理一系列插值问题，包括路径插值、迁移插值、嵌套插值、状态/迁移插值以及良基插值。通过详细描述这些插值问题及其Horn子句表示，我们希望促进一个通用的后端插值接口的出现，该接口可用于多种验证工具。
引用
@article{arxiv.1303.7378,
title = {Generalised Interpolation by Solving Recursion-Free Horn Clauses},
author = {Ashutosh Gupta and Corneliu Popeea and Andrey Rybalchenko},
journal= {arXiv preprint arXiv:1303.7378},
year = {2014}
}
备注
In Proceedings HCVS 2014, arXiv:1412.0825