Computing Over-Approximations with Bounded Model Checking

详细信息    查看全文

• 作者：Daniel Kroening
• 关键词：Bounded model checking ; SAT procedure ; safety property
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2006
• 出版时间：11 January 2006
• 年：2006
• 卷：144
• 期：1
• 页码：79-92
• 全文大小：264 K

文摘

Bounded Model Checking (BMC) searches for counterexamples to a property with a bounded length k. If no such counterexample is found, k is increased. This process terminates when k exceeds the completeness threshold 4J05Y68-7&_mathId=mml1&_user=3986987&_cdi=13109&_rdoc=7&_acct=C000050221&_version=1&_userid=10&md5=454799a26c77161c9770b823d7a6c1f3""> (i.e., k is sufficiently large to ensure that no counterexample exists) or when the SAT procedure exceeds its time or memory bounds. However, the completeness threshold is too large for most practical instances or too hard to compute.

Hardware designers often modify their designs for better verification and testing results. This paper presents an automated technique based on cut-point insertion to obtain an over-approximation of the model that 1) preserves safety properties and 2) has a which is small enough to actually prove using BMC. The algorithm uses proof-based abstraction refinement to remove spurious counterexamples.