fbPDR: In-depth combination of forward and backward analysis in Property Directed Reachability
Tobias Seufertna and Christoph Schollb
University of Freiburg, Germany
aseufert@informatik.uni-freiburg.de
bscholl@informatik.uni-freiburg.de
ABSTRACT
We describe a thoroughly interweaved forward and backward version of PDR/IC3 called fbPDR. Motivated by the complementary strengths of PDR and Reverse PDR and by related work showing the benefits of collaboration between the two, fbPDR lifts the combination to a new level. We lay the theoretical foundations for sharing information represented by learned lemmas between PDR and Reverse PDR and demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition.
