CHCs 的自下而上方法：线性约束 Horn 子句向软件验证的新型转换
计算机科学中的逻辑
2024-04-24 v1 软件工程
摘要
约束 Horn 子句（CHCs）传统上用作形式化验证的低级表示。大多数现有求解器使用多样化的专用技术，包括直接状态空间遍历或底层抽象化逼近， necessitating purpose-built complex algorithms。另一些求解器成功地通过将问题转换为其他验证任务的输入来简化验证工作流程，发挥现有算法的优势。一种方法将 CHC 问题转换为大约模拟自上而下求解器的递归程序；验证指定为控制位置的安全违规可达性。我们提出一种针对线性 CHCs 的替代自下而上方法，并在开源模型检查框架 THETA 中对两种方法进行评估，分别在人工合成和工业实例上进行测试。我们发现，当采用新颖的自下而上方法时，在验证工作流程中解决的任务数量增加了两倍以上，与自上而下技术形成鲜明对比。
关键词
引用
@article{arxiv.2404.15215,
title = {Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification},
author = {Márk Somorjai and Mihály Dobos-Kovács and Zsófia Ádám and Levente Bajczi and András Vörös},
journal= {arXiv preprint arXiv:2404.15215},
year = {2024}
}
备注
In Proceedings LSFA/HCVS 2023, arXiv:2404.13672. This research was partially funded by the UNKP-22-2,3-I New National Excellence Program and Project no. 2019-1.3.1-KK-2019-00004, which has been implemented with the support provided from the National Research, Development and Innovation Fund of Hungary, financed under the 2019-1.3.1-KK funding scheme