面向简单线性算术的带排序 Datalog 锤：监督器验证条件求解
计算机科学中的逻辑
2022-01-25 v1
摘要
在先前的工作中，我们证明了属于简单线性实数算术上的 Horn Bernays-Schönfinkel 片段（HBS(SLR)）的子句集可以转化为有限一阶常量集上的 HBS 子句集。该转化保持有效性和可满足性，并且当我们将输入扩展为带有正的全称或存在量词验证条件（猜想）时仍然适用。我们称这种转化为 Datalog 锤。其在 SPASS-SPL 中的实现与 Datalog 推理器 VLog 的结合，建立了一种判定 Horn 片段中验证条件的有效方法。我们针对两个示例验证了监督器代码：汽车中的车道变更辅助系统和增压内燃机的电子控制单元。在本文中，我们从多个方面改进了我们的 Datalog 锤：将其推广到混合实数-整数算术和有限一阶排序；将可接受不等式的类别扩展到变量边界和正接地不等式之外；并通过软类型规则显著减小了锤的输出规模。我们称结果为带排序的 Datalog 锤。它不仅使我们能够处理更复杂的监督器代码并更简洁地建模已考虑的监督器代码，还提高了我们在真实世界基准示例上的性能。最后，我们将 SPASS-SPL 与 VLog 之间先前基于文件的接口替换为紧密耦合，从而产生单一的可执行二进制文件。
引用
@article{arxiv.2201.09769,
title = {A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic},
author = {Martin Bromberger and Irina Dragoste and Rasha Faqeh and Christof Fetzer and Larry González and Markus Krötzsch and Maximilian Marx and Harish K Murali and Christoph Weidenbach},
journal= {arXiv preprint arXiv:2201.09769},
year = {2022}
}
备注
34 pages, to be published in the proceedings for TACAS 2022. arXiv admin note: text overlap with arXiv:2107.03189