Bounded model checking
Bounded model checking
复制标题
DOI：
10.1016/s0065-2458(03)58003-2
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Armin Biere
中科院分区：
文献类型：
--
作者：
Armin Biere
目前，SAT最重要的工业应用之一是有界模型检查（BMC）。这种技术通常用于电子设计自动化背景下的正式硬件验证。但BMC也成功地应用于许多其他领域。在实践中，BMC主要用于伪造，这涉及到违反时间属性。此外，本章的相当一部分讨论了完全扩展，包括k-归纳和插值。这些扩展也允许证明属性。
One of the most important industrial applications of SAT is currently Bounded Model Checking (BMC). This technique is typically used for formal hardware verification in the context of Electronic Design Automation. But BMC has successfully been applied to many other domains as well. In practice, BMC is mainly used for falsification, which is concerned with violations of temporal properties. In addition, a considerable part of this chapter discusses complete extensions, including k-induction and interpolation. These extensions also allow to prove properties.