Name
Abstract | ||
|---|---|---|
Temporal induction is a SAT-based model checking technique. We prove that the SAT instances generated by its induction rule can be reduced to the so called Incremental CNFs. A new DPLL procedure is customized for Incremental CNFs, so that the intermediate results in solving previous instances, including the learnt clauses and the search tree, can be reused in solving the next instance. To the best of our knowledge, this is the first result on reusing the search tree in SAT solving of temporal induction. Experimental results on a large number of benchmarks show significant performance gain of our approach. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/ICECCS.2013.21 | ICECCS |
Keywords | Field | DocType |
incremental cnfs,induction rule,sat-based model checking technique,learnt clause,temporal induction,sat based model checking technique,incremental sat,reusing search tree,large number,search problems,incremental sat solving,sat instance,bounded model checking,search tree,incremental cnf,formal verification,intermediate result,model checking,benchmark testing | Incremental heuristic search,Model checking,Computer science,Algorithm,Theoretical computer science,Software,DPLL algorithm,Benchmark (computing),Formal verification,Search tree,Incremental decision tree | Conference |
ISBN | Citations | PageRank |
978-0-7695-5007-7 | 0 | 0.34 |
References | Authors | |
14 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Liangze Yin | 1 | 26 | 9.47 |
| Fei He | 2 | 175 | 28.32 |
| Min Zhou | 3 | 69 | 22.62 |
| Ming Gu | 4 | 554 | 74.82 |