@Article{AbrahamEA09,
  author =       "Erika {\'A}brah{\'a}m and Tobias Schubert and Bernd
                 Becker and Martin Fr{\"a}nzle and Christian Herde",
  title =        "Parallel {SAT} Solving in Bounded Model Checking",
  journal =      "Journal of Logic and Computation",
  year =         "2009",
  publisher =    "Oxford University Press",
  URL =          "http://dx.doi.org/10.1093/logcom/exp002",
  subproject=    {H1/2},
  access=        {restricted},
  bibtex=        {abraham.jlc2009.bib},
  pdf=           {abraham.jlc2009.pdf},
  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.",
  keywords =     "parallel programs, bounded model checking, SAT
                 solving, linear programming, hybrid systems",
}