首页 | 本学科首页   官方微博 | 高级检索  
     


Computing Over-Approximations with Bounded Model Checking
Authors:Daniel Kroening
Affiliation:Computer Science Department, ETH Zürich, Switzerland
Abstract:Bounded Model Checking (BMC) searches for counterexamples to a property phi with a bounded length k. If no such counterexample is found, k is increased. This process terminates when k exceeds the completeness threshold View the MathML source (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 View the MathML source which is small enough to actually prove phi using BMC. The algorithm uses proof-based abstraction refinement to remove spurious counterexamples.
Keywords:Bounded model checking   SAT procedure   safety property
本文献已被 ScienceDirect 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号