Interpolants And Symbolic Model Checking
VMCAI'07: Proceedings of the 8th international conference on Verification, model checking, and abstract interpretation（2007）
摘要
An interpolant for a mutually inconsistent pair of formulas (A, B) is a formula that is (1) implied by A, (2) inconsistent with B and (3) expressed over the common variables of A and B. An interpolant can be efficiently derived from a refutation of A A B, for certain theories and proof systems. In this tutorial we will cover methods of generating interpolants, and applications of interpolants, including invariant generation and abstraction refinement.
更多查看译文
关键词
inconsistent pair,abstraction refinement,certain theory,common variable,invariant generation,proof system,symbolic model checking
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要