loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Seventh International Workshop on Microprocessor Test and Verification (MTV'06)
Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs
Austin, Texas
December 04-December 05
ISBN: 0-7695-2839-2
ASCII Text
x 
 
Marc Herbstritt, Bernd Becker, Christoph Scholl, "Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs," Microprocessor Test and Verification, International Workshop on, pp. 37-44, Seventh International Workshop on Microprocessor Test and Verification (MTV'06), 2006.
 
 
BibTex
x
 
@article{ 10.1109/MTV.2006.3,
author = {Marc Herbstritt and Bernd Becker and Christoph Scholl},
title = {Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs},
journal ={Microprocessor Test and Verification, International Workshop on},
volume = {0},
year = {2006},
issn = {1550-4093},
pages = {37-44},
doi = {http://doi.ieeecomputersociety.org/10.1109/MTV.2006.3},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Microprocessor Test and Verification, International Workshop on
TI - Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs
SN - 1550-4093
SP37
EP44
A1 - Marc Herbstritt,
A1 - Bernd Becker,
A1 - Christoph Scholl,
PY - 2006
KW - null
VL - 0
JA - Microprocessor Test and Verification, International Workshop on
ER -
 
Marc Herbstritt, Albert-Ludwigs-University, Germany
Bernd Becker, Albert-Ludwigs-University, Germany
Christoph Scholl, Albert-Ludwigs-University, Germany
In this paper we will present an optimized structural 01X-SAT-solver for bounded model checking of blackbox designs that exploits semantical knowledge regarding the node selection during SAT search. Experimental results show that exploiting the problem structure in this way speeds up the 01X-SAT-solver considerably. Additionally, we give a concise first-order formulation that is more expressive than using 01X-logic. This formulation leads to hard-to-solve QBF formulas for which experimental results from the QBF Evaluation 2006 are presented.
Citation:
Marc Herbstritt, Bernd Becker, Christoph Scholl, "Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs," mtv, pp.37-44, Seventh International Workshop on Microprocessor Test and Verification (MTV'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.