loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2009 IEEE/IFIP International Symposium on Rapid System Prototyping
WoLFram- A Word Level Framework for Formal Verification
Paris, France
June 23-June 26
ISBN: 978-0-7695-3690-3
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.
Index Terms:
Formal Verification, Boolean SAT, Satisfiable Modulo Theories (SMT)
Citation:
André Sülflow, Ulrich Kühne, Görschwin Fey, Daniel Große, Rolf Drechsler, "WoLFram- A Word Level Framework for Formal Verification," rsp, pp.11-17, 2009 IEEE/IFIP International Symposium on Rapid System Prototyping, 2009
Usage of this product signifies your acceptance of the Terms of Use.