Input-based Three-valued Abstraction Refinement
Jan Onderka and Stefan Ratschan
与反例引导抽象精炼(CEGAR)不同,三有价值的抽象精炼(TVAR)能够验证mu-calculus的所有属性。 我们为TVAR提出了一种新的算法框架,它采用类似模拟器的方法,通过基于输入的拆分来构建和完善抽象状态空间。 这导致了一种状态空间形式主义,它比以前使用模态转换的TVAR框架要简单得多。 我们在AVR架构的机床检查和机器代码系统的验证属性中实现了框架,展示了验证系统和mu-calculus属性的能力,这些属性不是通过天真的模型检查或CEGAR分别可以验证的。 这是 TVAR 首次用于机器代码验证。
Unlike Counterexample-Guided Abstraction Refinement (CEGAR), Three-Valued Abstraction Refinement (TVAR) is able to verify all properties of the mu-calculus. We present a novel algorithmic framework for TVAR that employs a simulator-like approach to build and refine the abstract state space with input-based splitting. This leads to a state space formalism that is much simpler than in previous TVAR frameworks, which use modal transitions. We implemented the framework in our open-source tool machin...