电子笔记在理论计算机科学56（2001）http://www.elsevier.nl/locate/entcs/volume56.html190页形式化验证基于布尔表达式图保罗·弗雷德里克·威廉姆斯c2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。摘要本文研究了布尔表达式图（BED）在形式验证领域中的应用。最近开发的数据结构允许快速和有效的操作布尔公式。形式验证中的许多问题都可以转化为布尔公式问题。我们选择了一些这样的问题，并显示如何解决他们使用床。组合电路的等价性检验是一个形式化的验证问题，它可以转化为布尔公式的重言式检验。我们- ING床，我们能够保持布尔公式内的电路的大部分结构。我们展示了如何利用结构信息的验证过程中。有时，组合电路是以层次或模块的方式指定的。我们提出了一种方法来验证两个这样的电路之间的等价性。该方法建立在切割传播上。假设两个电路的输入相同，我们通过电路从输入到输出传播这个知识。结果是知道两个电路的输出如何对应，例如，这两个电路的输出是否成对相等？切割的回路和运动可以用布尔公式来描述。符号模型检验是一种用于验证nite状态机的时态规范的技术。 众所周知，如何可以使用布尔公式来表达nite状态机和时间规格的评估。我们将展示如何使用床进行这些操作。我们专注于标准的符号模型检测方法是很难的例子。判断公式是否满足是组合电路验证和符号模型检验中的一个问题。通常，满意度检查与发现错误有关。我们将研究如何使用BED数据结构进行满意度检查最后，我们来看看如何扩展BED数据IIIIV结构在其他操作中，我们介绍了一个操作，用于计算故障树中的最小p-割。故障树是一个布尔公式，它根据每个组件的状态（“故障”或“工作”）来表示系统是否发生故障。最小p截是系统故障最可能的原因的表示。该方法可用于在给定每个部件的失效概率的情况下近似计算系统失效概率。作为这项研究的一部分，我们开发了一个床包。附件从用户的角度描述了软件包。在打印这本书是对作者的博士论文的稍加修改。 [Wil00]。
