Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1109/MTV.2006.3 | MTV |
Keywords | Field | DocType |
concise first-order formulation,blackbox design,qbf evaluation,semantical knowledge,advanced sat-techniques,bounded model checking,blackbox designs,problem structure,sat search,qbf formula,node selection,first order,formal verification,sat solver,boolean functions,logic design,formal specification,computability | Boolean function,Logic synthesis,Model checking,Logic testing,Computer science,Algorithm,Formal specification,Computability,Theoretical computer science,Bounded function,Formal verification | Conference |
ISBN | Citations | PageRank |
0-7695-2839-2 | 18 | 0.88 |
References | Authors | |
16 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marc Herbstritt | 1 | 136 | 11.01 |
| Bernd Becker | 2 | 18 | 0.88 |
| Christoph Scholl | 3 | 346 | 32.07 |