广义符号化轨迹评估的忠实语义
计算机科学中的逻辑
2015-07-01 v2
摘要
广义符号化轨迹评估(GSTE)是一种高容量的硬件形式化验证技术。GSTE使用抽象化，这意味着电路行为的细节会从电路模型中被移除。GSTE的语义可用于预测和理解为何某些电路属性能被或不能被GSTE证明。已有若干种为GSTE描述的语义。然而，这些语义对于GSTE算法的证明能力并不忠实，即GSTE算法相对于这些语义是不完备的。GSTE中使用的抽象化使得理解为何某个特定属性能被或不能被GSTE证明变得困难。上述语义无法帮助用户做到这一点。本文的贡献在于为GSTE提供了一种忠实语义。也就是说，我们给出一个简单的形式化理论，该理论认为一个属性为真当且仅当该属性能被GSTE模型检验器证明。我们证明了GSTE算法相对于该语义是可靠且完备的。
引用
@article{arxiv.0901.2518,
title = {A Faithful Semantics for Generalised Symbolic Trajectory Evaluation},
author = {Koen Claessen and Jan-Willem Roorda},
journal= {arXiv preprint arXiv:0901.2518},
year = {2015}
}