Complementary Approximate Reachability (CAR)

CAR is SAT-based safety model checking technique inspired by the classic reachability analysis. As the reachability analysis allows both forward and backward search, CAR also has both the forward and backward versions. From our current evaluations, backward CAR performs better than forward CAR. Compared to other SAT-based model checking techniques, the contributions of CAR are as follows.

  • CAR can find bugs that cannot be found by BMC or IC3. (see our CAV 2018 paper)
  • CAR can prove models that cannot be proved by IMC or IC3. (see our ICCAD 2017 paper)

Publications (ordered by year):

  • Intersection and Rotation of Assumption Literals Boosts Bug-Finding. VSTTE 2019. pdf
  • SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability. CAV 2018. pdf
  • Safety Model Checking with Complementary Approximations. ICCAD 2017. pdf

Tool:

  • simplecar : a simple and efficient implementation of CAR.

Open questions:

  1. Can CAR do better than the state-of-the-art bug finding technique BMC (Bounded Model Checking)?
  2. What is the relationship between CAR and IC3?
  3. Can we apply AI search strategies such as A* or machine learning mechanism to improve the performance of CAR?
  4. How hard is it to shift CAR from the bit-level (SAT-based) to the word-level (SMT-based)?