Sciweavers

MTV
2006
IEEE

Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs

13 years 9 months ago
Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs
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.
Marc Herbstritt, Bernd Becker, Christoph Scholl
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where MTV
Authors Marc Herbstritt, Bernd Becker, Christoph Scholl
Comments (0)