基于EUF的NRA迁移系统增量约简为LRA的不变性检验
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
摘要：
用非线性实算术（NRA）检验设计（表示为转移系统）的模型检验不变性质是一个重要而又困难的问题。一方面，NRA是一个难以解决的理论，另一方面，大多数强大的模型检验技术缺乏对NRA的支持。在本文中，我们提出了一个反例引导的抽象细化（CEGAR）的方法，利用微分的线性化技术，使使用成熟和有效的模型检验算法的过渡系统的线性实数运算（LRA）与未解释的功能（EUF）。实证评估的结果证实了这种方法的有效性和潜力。
英文摘要：
Model checking invariant properties of designs, represented as transition systems, with non-linear real arithmetic (NRA), is an important though very hard problem. On the one hand NRA is a hard-to-solve theory; on the other hand most of the powerful model checking techniques lack support for NRA. In this paper, we present a counterexample-guided abstraction refinement (CEGAR) approach that leverages linearization techniques from differential calculus to enable the use of mature and efficient model checking algorithms for transition systems on linear real arithmetic (LRA) with uninterpreted functions (EUF). The results of an empirical evaluation confirm the validity and potential of this approach.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
