基于不可满足核的近似逼近可达性分析

In recent years, formal verification technology has received more and more attention, and it plays an important role in ensuring the safety and correctness of systems in critical areas of safety. As a branch of formal verification with a high degree of automation, model checking has a very broad development prospect. In this paper, we study and propose a new model checking technique, which can effectively check transition systems, including bug-finding and safety proof. Different from existing model checking algorithms, our proposed method, UC-based approximate incremental reachability (UAIR) based on unsatisfiable core (UC), mainly utilizes the unsatisfiable core to solve a series of candidate safety invariants until the final invariant is generated, so as to realize safety proof and bug-finding. In symbolic model checking based on the SAT solver, we use the UC obtained by the satisfiability solver to construct candidate safety invariant, and if the transition system itself is safe, the initial invariant we get is only an approximation of the safety invariant. Then, while checking the safety, we gradually improve the candidate safety invariant until we find a real invariant that proves the system is safe; if the system is unsafe, our method can finally find a counterexample to prove the system is unsafe. As a brand new method, we exploit unsatisfiable cores for safety model checking and achieve quite good results. As we all know, there is no absolute best method in the field of model checking, although our method cannot surpass the current mature methods such as IC3, CAR, etc, it is believed that this method can be a valuable addition to the model checking toolset.