WoLFram- A Word Level Framework for Formal Verification
WoLFram- A Word Level Framework for Formal Verification
复制标题
WoLFram - 用于形式验证的字级框架
DOI：
10.1109/rsp.2009.21
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
André Sülflow
中科院分区：
文献类型：
--
作者：
André Sülflow
针对纯布尔级形式验证计算量大的问题，提出了可满足性模理论(SMT)等词级证明技术。最初基于布尔可满足性(SAT)的验证方法可以直接受益于这一进展。在这项工作中，我们提出了词级框架Wolfram，它允许开发独立于底层证明技术的系统形式化验证应用程序。该框架分为应用层、核心引擎和后端层。实现了广泛的应用，例如等价性和属性检查，包括覆盖/属性分析、调试和健壮性检查的算法。后端支持布尔和词级技术，如SMT和约束求解(CSP)。这使得Wolfram成为开发和快速评估新出现的核查技术的稳定支柱。
Due to high computational costs of formal verification on pure Boolean level, proof techniques on the word level, like Satisfiability Modulo Theories (SMT), were proposed. Verification methods originally based on Boolean satisfiability (SAT) can directly benefit from this progress. In this work we present the word level framework WoLFram that enables the development of applications for formal verification of systems independent of the underlying proof technique. The framework is partitioned into an application layer, a core engine and a back-end layer. A wide range of applications is implemented, e.g.~equivalence and property checking including algorithms for coverage/property analysis, debugging and robustness checking. The back-end supports Boolean as well as word level techniques, like SMT and Constraint Solving (CSP). This makes WoLFram a stable backbone for the development and quick evaluation of emerging verification techniques.