Search

Abstract: Increasing attention has been paid recently to criteria that allow one to conclude that a structure models a linear-time property from the knowledge that no counterexamples exist up to a certain length. These termination criteria effectively turn Bounded Model Checking into a full-fledged verification technique and sometimes result in considerable time savings. In [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV''04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] we presented a criterion based on the translation of the linear-time specification into a Büchi automaton. BMC can be terminated if no fair cycle is found up to a given length, and one can prove that no fair cycle exists beyond that length. The maximum length for which counterexamples are explicitly checked is called the termination length; it obviously depends on the model, the property, and the termination criterion. In this paper we improve the criterion of [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV''04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] by adding a check that often substantially reduces termination length. Our previous work employed translation to a non-generalized Büchi automaton. Though a well-known technique converts a generalized automaton into that form by composing it with a counter, it has the undesirable effect of considerably lengthening the cycles in the graph to be searched. We propose several alternatives to that approach and compare them experimentally. The translation to automata can be accomplished in more than one way, and in this paper we contrast two of them: one based on the algorithms of [F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In E. A. Emerson and A. P. Sistla, editors, Twelfth Conference on Computer Aided Verification (CAV''00), pages 248–263. Springer-Verlag, Berlin, July 2000. LNCS 1855], and one based on the notion of tight automaton of [E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV''94), pages 415–427. Springer-Verlag, Berlin, 1994. LNCS 818]. The latter yields shorter counterexamples, but the former often leads to earlier termination. In addition, it can help in identifying safety properties, for which termination checks are much more efficient than for the general case. We finally present results on comparing techniques based on cycle detection to the technique of [V. Schuppan and A. Biere. Efficient reduction of finite state model checking to reachability analysis. Software Tools for Technology Transfer, 5(2–3):185–204, Mar. 2004], which converts liveness properties into safety properties by augmentation of the model. [Copyright &y& Elsevier]

Abstract: In Bounded Model Checking (BMC), the search for counterexamples of increasing lengths is translated into a sequence of satisfiability (SAT) checks. It is natural to try to exploit the similarity of these SAT instances by forwarding clauses learned during conflict analysis from one instance to the next. The methods proposed to identify clauses that remain valid fall into two categories: Those that are oblivious to the mechanism that generates the sequence of SAT instances and those that rely on it. In the case of a BMC run, it was observed by Strichman [O. Shtrichman. Pruning techniques for the SAT-based bounded model checking problem. In Correct Hardware Design and Verification Methods (CHARME 2001), pages 58–70, Livingston, Scotland, Sept. 2001. Springer. LNCS 2144] that those clauses learned during one SAT check that only depend on the structure of the model remain valid when checking for longer counterexamples. Eén and Sörensson [N. Eén and N. Sörensson. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 89(4), 2003. First International Workshop on Bounded Model Checking. http://www.elsevier.nl/locate/entcs/] pointed out that all learned clauses can be forwarded if the translation into SAT obeys commonly followed rules. Many clauses that are forwarded this way, however, are of little usefulness and may degrade performance. This paper presents an extension to Strichman''s approach in the form of a more general criterion to filter conflict clauses that can be profitably forwarded to successive instances. This criterion, in particular, is still syntactic and quite efficient, but accounts for the presence of both primary and auxiliary objectives in the SAT instance. This paper also introduces a technique to distill clauses to be forwarded even though they fail the syntactic check. Distillation is a semantic approach that can be applied in general to incremental SAT, and often produces clauses that are independent of the primary objective, and hence remain valid for the remainder of the sequence of instances. In addition, distillation often improves the quality of the clauses, that is, their ability to prevent the examination of large regions of the search space. Experimental results obtained with the CirCUs SAT solver confirm the efficacy of the proposed techniques, especially for large, hard problems. [Copyright &y& Elsevier]

We present an abstraction refinement algorithm for model checking of safety properties that relies exclusively on a SAT solver for checking the abstract model, testing abstract counterexamples on the concrete model, and refinement. Model checking of the abstractions is based on bounded model checking extended with checks for the existence of simple paths that help in deciding passing properties. All minimum-length spurious counterexamples are eliminated in one refinement step by a procedure that combines the analysis of the conflict dependency graph produced by the SAT solver while looking for concrete counterexamples with an effective abstraction minimization procedure. [Copyright &y& Elsevier]