bradleySATBasedModelChecking2011:
  type: article
  title: '{SAT-Based Model Checking} without {Unrolling}'
  author: Bradley, Aaron
  date: 2011-01-23
  page-range: 70-87
  serial-number:
    doi: 10.1007/978-3-642-18275-4_7
    isbn: 978-3-642-18274-7
  abstract: 'A new form of SAT-based symbolic model checking is described. Instead of unrolling the transition relation, it incrementally generates clauses that are inductive relative to (and augment) stepwise approximate reachability information. In this way, the algorithm gradually refines the property, eventually producing either an inductive strengthening of the property or a counterexample trace. Our experimental studies show that induction is a powerful tool for generalizing the unreachability of given error states: it can refine away many states at once, and it is effective at focusing the proof search on aspects of the transition system relevant to the property. Furthermore, the incremental structure of the algorithm lends itself to a parallel implementation.'
  parent:
    type: proceedings
    title: Verification, Model Checking, and Abstract Interpretation (VMCAI 2011)
    volume: 6538
    parent:
      type: proceedings
      title: Lecture Notes in Computer Science