基于增量归约为带 EUF 的 LRA 的 NRA 迁移系统不变性检查
计算机科学中的逻辑
2018-01-29 v1
摘要
以迁移系统表示、具有非线性实算术（NRA）的设计的不变性质模型检查是一个重要但极难的问题。一方面 NRA 是难以求解的理论；另一方面大多数强大的模型检查技术缺乏对 NRA 的支持。本文提出一种反例引导的抽象精化（CEGAR）方法，利用微分学中的线性化技术，使得成熟的、高效的针对带未解释函数（EUF）的线性实算术（LRA）迁移系统的模型检查算法得以应用。实证评估结果证实了该方法的有效性与潜力。
引用
@article{arxiv.1801.08718,
title = {Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF},
author = {Alessandro Cimatti and Alberto Griggio and Ahmed Irfan and Marco Roveri and Roberto Sebastiani},
journal= {arXiv preprint arXiv:1801.08718},
year = {2018}
}