基于模板的多项式程序 LTL 属性验证的可靠且完备见证
编程语言
2024-07-02 v3 计算机科学中的逻辑
摘要
我们研究了针对线性时序逻辑（LTL）形式规范验证程序的经典问题。我们首先提出了用于命令式程序 LTL 验证的新型可靠且完备的见证（witnesses）。我们的见证既适用于验证（证明）场景，也适用于反驳（发现错误）场景。随后，我们考虑原子命题可为多项式约束的 LTL 公式，并将重点转向多项式算术程序，即每个赋值和守卫仅由多项式表达式构成的程序。针对该设定，我们提供了一种高效算法以自动综合此类 LTL 见证。我们的综合过程既是可靠的也是半完备的。最后，我们展示了实验结果，证明了该方法的有效性，并表明其能够处理以往最先进工具无法触及的程序。
引用
@article{arxiv.2403.05386,
title = {Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs},
author = {Krishnendu Chatterjee and Amir Kafshdar Goharshady and Ehsan Kafshdar Goharshady and Mehrdad Karrabi and Đorđe Žikelić},
journal= {arXiv preprint arXiv:2403.05386},
year = {2024}
}