Horn子句验证中的凸多面体抽象、特殊化和基于属性的谓词分裂
计算机科学中的逻辑
2014-12-04 v1
摘要
我们提出了一种约束Horn子句（CHC）验证方法，结合了三种技术：凸多面体域上的抽象解释、使用查询-答案转换子句的抽象解释对CHC中的约束进行特殊化，以及通过分裂谓词进行精化。本工作的目的是研究为约束逻辑程序（CLP）开发的分析和转换工具如何应用于Horn子句验证问题。凸多面体上的抽象解释能够推导出复杂的不变式，当与用于传播约束的特殊化结合使用时，通常可以解决具有挑战性的验证问题。这本身就是一个贡献，但当它失败时需要精化，而如何精化凸多面体分析的问题尚未得到充分研究。我们提出了一种基于反例轨迹导出的插值的精化技术；这些插值用于驱动基于属性的特殊化，从而分裂谓词，进而导致更精确的凸多面体分析。特殊化、分析和分裂的过程可以重复，类似于CEGAR和迭代特殊化方法。
引用
@article{arxiv.1412.1154,
title = {Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification},
author = {Bishoksan Kafle and John P. Gallagher},
journal= {arXiv preprint arXiv:1412.1154},
year = {2014}
}
备注
In Proceedings HCVS 2014, arXiv:1412.0825