面向数据库驱动验证的量词消去
计算机科学中的逻辑
2019-06-18 v2
摘要
在数据库驱动系统中运行验证任务需要求解一种新型的量词消去问题。这些量词消去问题与 Gulwani 和 Musuvathi 在 ESOP 2008 中引入的覆盖(cover)概念相关。在本文中,我们展示了覆盖与模型完备化(model completions)这一模型论中众所周知的主题严格相关。我们还通过采用带约束版本的 Superposition Calculus,并配备适当的设置与归约策略,研究了覆盖在其中的计算。此外,我们表明对于数据库驱动验证应用中使用的语言片段,覆盖计算在计算上是易处理的。通过使用 MCMT 工具对数据感知过程基准进行验证所获得的初步结果分析,证实了这一观察。这些基准可在该工具分发的最后版本中找到。
引用
@article{arxiv.1806.09686,
title = {Quantifier Elimination for Database Driven Verification},
author = {Diego Calvanese and Silvio Ghilardi and Alessandro Gianola and Marco Montali and Andrey Rivkin},
journal= {arXiv preprint arXiv:1806.09686},
year = {2019}
}