Qf_bv Model Checking With Property Directed Reachability
DATE '13: Proceedings of the Conference on Design, Automation and Test in Europe(2013)
摘要
In 2011, property directed reachability (PDR) was proposed as an efficient algorithm to solve hardware model checking problems. Recent experimentation suggests that it outperforms interpolation-based verification, which had been considered the best known algorithm for this purpose for almost a decade. In this work, we present a generalization of PDR to the theory of quantifier free formulae over bitvectors (QF_BV), illustrate the new algorithm with representative examples and provide experimental results obtained from experimentation with a prototype implementation.
更多查看译文
关键词
efficient algorithm,known algorithm,new algorithm,recent experimentation,experimental result,hardware model checking problem,interpolation-based verification,prototype implementation,quantifier free formula,representative example,QF BV model checking
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要