论文部分内容阅读
有界模型校验（Bounded Model Checking）由于验证的不完备性而经常受到验证人员的指责。为了解决这个问题，计算时序深度的算法被提出。该文算法基于可满足性算法引擎，与其它基于可满足性算法引擎的算法不同，为了减少可满足性算法引擎的负担，采用了状态空间显式存储的方法。ISCAS’89的实例很好证明了该算法的有效性。