Name
Abstract | ||
|---|---|---|
Bounded Model Checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1093/logcom/exp002 | Journal of Logic and Computation |
Keywords | Field | DocType |
Parallel programs,bounded model checking,SAT solving,linear programming,hybrid systems | Model checking,Computer science,Satisfiability,Theoretical computer science,Conjunctive normal form,Counterexample,Solver,Bounded function,Hybrid automaton | Conference |
Volume | Issue | ISSN |
21 | 1 | 0955-792X |
Citations | PageRank | References |
6 | 0.47 | 20 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Erika Ábrahám | 1 | 830 | 63.17 |
| Tobias Schubert | 2 | 598 | 37.74 |
| Bernd Becker | 3 | 6 | 0.47 |
| Martin Fränzle | 4 | 786 | 61.58 |
| Christian Herde | 5 | 338 | 15.19 |