Abstract We present , a new SAT-based model-checking algorithm for the verification of liveness properties of finite-state symbolic transition systems. Like other recent approaches, works by reducing liveness checking to a sequence of safety checks. Similarly to , it incrementally strengthens the input system using constraints obtained by refuting candidate counterexamples to the input liveness property, assumed (w.l.o.g.) to be of the form FGq. Differently from (and crucially), however, instead of directly searching for lasso-shaped counterexamples visiting $$\lnot q$$ ¬ q infinitely-often, searches for counterexamples incrementally, via a recursive chain of safety checks, each of which tries to determine whether it is possible to reach a $$\lnot q$$ ¬ q -state from a given $$\lnot q$$ ¬ q -state (which was previously determined to be reachable), in a manner similar to . When the current candidate counterexample is refuted, exploits the inductive invariants generated by the (recursive) safety checks to restrict the search space, until either no more reachable $$\lnot q$$ ¬ q -states remain, or a real lasso-shaped counterexample is found. In this paper, we describe in detail, prove its soundness and completeness, and compare it against the state of the art both theoretically and empirically. Our experimental results show that our implementation of outperforms state-of-the-art implementations of , and other SAT-based liveness checking algorithms on a wide range of benchmarks from the literature.

Abstract / and its variants have been the prominent approaches to safety model checking in recent years. Compared to the previous model-checking algorithms like (Bounded Model Checking) and (Interpolation Model Checking), / is attractive due to its completeness (vs. ) and scalability (vs. ). / maintains an over-approximate state sequence for proving the correctness. Although the sequence refinement methodology is known to be crucial for performance, the literature lacks a systematic analysis of the problem. We propose an approach based on the definition of i- good lemmas, and the introduction of two kinds of heuristics, i.e., and , to steer the search towards the construction of $$i$$ -good lemmas. The approach is applicable to and its variant (Complementary Approximate Reachability), and it is very easy to integrate within existing systems. We implemented the heuristics into two open-source model checkers, and , as well as into the mature platform, and carried out an extensive experimental evaluation on HWMCC benchmarks. The results show that the proposed heuristics can effectively compute more $$i$$ -good lemmas, and thus improve the performance of all the above checkers.

Model checking is an automatic formal verification method that is widely applied to hardware verification. Safety properties are the mainly verified properties in practice that can be falsified within finite steps if they do not hold for systems. However, state-of-the-art safety model-checking algorithms cannot meet the performance requirement driven by the industry as the sizes of (hardware) systems to be verified increase rapidly. Therefore, more efficient techniques are still eagerly in demand. Recently, a new safety model-checking technique complementary approximate reachability (CAR) was presented and received considerable concerns from the community. CAR has shown its advantages in unsafe checking (bug finding), but cannot be as competitive as other state-of-the-art techniques, e.g., IC3/PDR, on safe checking (proving correctness). In this article, we propose four kinds of heuristics, two inspired by IC3/PDR and another two dedicated to CAR, to improve the performance of CAR. We integrate the heuristics into the open-source model checker SimpleCAR and compare the performance to the original CAR and IC3/PDR on 748 instances from the hardware model-checking competitions. Our results show that by fixing the time and memory resources, CAR can solve 124 more instances with the four proposed heuristics, i.e., 53.4% more instances can be solved comparing to the original CAR. Furthermore, CAR in both forward and backward directions can solve ten more instances than IC3/PDR in corresponding directions, and uniquely solve 44 more instances that IC3/PDR in corresponding directions cannot solve, which increases the capability of the current model-checking portfolio.