Model checking is an automatic formal verification technique that is widely used in hardware verification. The state-of-the-art complete model-checking techniques, based on IC3/PDR and its general variant CAR, are based on computing symbolically sets of under- and over-approximating state sets (called “frames”) with multiple calls to a SAT solver. The performance of those techniques is sensitive to the order of the assumptions with which the SAT solver is invoked, because it affects the unsatisfiable cores that it emits if the formula is unsatisfiable—which the solver emits when the formula is unsatisfiable—that crucially affect the search process. This observation was previously published (Dureja et al., 2020), where two partial assumption ordering strategies, intersection and rotation were suggested (partial in the sense that they determine the order of only a subset of the literals). In this article we extend and improve these strategies based on an analysis of the reason for their effectiveness. We prove that intersection is effective because of what we call locality of the cores, and our improved strategy is based on this observation. We conclude our paper with an extensive empirical evaluation of the various ordering techniques. One of our strategies, Hybrid-CAR, which switches between strategies at runtime, not only outperforms other, fixed ordering strategies, but also outperforms other state-of-the-art bug-finding algorithms, such as ABC-BMC.

Bounded Model Checking (BMC) is so far considered as the best engine for bug-finding in hardware model checking. Given a bound K, BMC can detect if there is a counterexample to a given temporal property within K steps from the initial state, thus performing a global-style search. Recently, a SAT-based model-checking technique called Complementary Approximate Reachability (CAR) was shown to be complementary to BMC, in the sense that frequently they can solve instances that the other technique cannot, within the same time limit. CAR detects a counterexample gradually with the guidance of an over-approximating state sequence, and performs a local-style search. In this paper, we consider three different ways to combine BMC and CAR. Our experiments show that they all outperform BMC and CAR on their own, and solve instances that cannot be solved by these two techniques. Our findings are based on a comprehensive experimental evaluation using the benchmarks of two hardware model checking competitions.

Abstract When synthesizing a system from a given specification, there is room for automatically adding various requirements, hence improving the resulting system. One such requirement covered extensively in past literature is that of robustness. In particular, the system can fail to read the inputs correctly from the environment, and the environment can fail to satisfy our assumptions about its behavior. Nevertheless, we want the system to still satisfy the specification even under these failures, in some limited way. It has to be limited because it is typically too strong of a requirement to realize the property regardless of the inputs and the environment’s assumptions. In this work, we propose a simple and flexible framework for synthesizing robust systems, where the user defines the required robustness via a temporal robustness specification. For example, the user may specify that the environment is eventually reliable, or input misreadings cannot occur more than $$k$$ k consecutive steps and synthesize a system under this assumption. Furthermore, our framework enables us to specify a temporal recovery specification, which describes how the designer expects the system to recover after a failure of the environment assumptions. We show examples of robust systems that we synthesized with this method using our synthesis tool Party.

Abstract In reactive synthesis, one begins with a temporal specification $$\varphi $$ φ , and automatically synthesizes a system $$M$$ M such that $$M\models \varphi $$ M ⊧ φ . As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies $$\varphi $$ φ non-vacuously, then M is likely to be closer to the user’s intent, because it satisfies $$\varphi $$ φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.

We propose to use algorithms for learning deterministic finite automata (DFA), such as Angluin’s L* algorithm, for learning a DFA that describes the possible scenarios under which a given program error occurs. The alphabet of this automaton is given by the user (for instance, a subset of the function call sites or branches), and hence the automaton describes a user-defined abstraction of those scenarios. More generally, the same technique can be used for visualising the behavior of a program or parts thereof. It can also be used for visually comparing different versions of a program (by presenting an automaton for the behavior in the symmetric difference between them), and for assisting in merging several development branches. We present experiments that demonstrate the power of an abstract visual representation of errors and of program segments, accessible via the project’s web page. In addition, our experiments in this paper demonstrate that such automata can be learned efficiently over real-world programs. We also present lazy learning, which is a method for reducing the number of membership queries while using L*, and demonstrate its effectiveness on standard benchmarks.

Past literature on synthesis identified the need to synthesize systems that are robust to failures of the system in reading the inputs from the environment, and also to failures of the environment itself to satisfy our assumptions about its behavior. In this work, we propose a simple and flexible framework for synthesizing robust systems, where the user defines the required robustness via a temporal robustness specification. For example, the user may specify that the environment is eventually reliable, or input misreadings cannot occur more than k consecutive steps, and synthesize a system under this assumption. Furthermore, our framework enables us to specify, also, a temporal recovery specification, i.e., describing the way the system is expected to recover after a failure of the environment assumptions. We show examples of robust systems that we have synthesized with this method by our synthesis tool PARTY.

Finding a minimal (i.e., irreducible) unsatisfiable core (MUC), and high-level minimal unsatisfiable core (also known as group MUC, or GMUC), are well-studied problems in the domain of propositional satisfiability. In contrast, in the domain of SMT, no solver in the public domain produces a minimal or group-minimal core. Several SMT solvers, like Z3, produce a core but do not attempt to minimize it. The SMT solver MATHSAT has an option to try to make the core smaller, but does not guarantee minimality. In this article we present a method and tool, HSMTMUC, for finding MUC and GMUC for SMT solvers. The method is based on the well-known deletion-based MUC extraction that is used in most propositional MUC extractors, together with several new optimizations such as theory-rotation, and an adaptive activation strategy based on measurements, during execution, of the time consumed by various components, combined with exponential smoothing. We implemented HSMT-MUC on top of Z3 and MATHSAT, and evaluated its performance with hundreds of SMT-LIB benchmarks.

Model counting is the #P problem of counting the number of satisfying solutions of a given propositional formula. Here we focus on a restricted variant of this problem, where the input formula is monotone (i.e., there are no negations). A monotone conjunctive normal form (CNF) formula is sufficient for modeling various graph problems, e.g., the vertex covers of a graph. Even for this restricted case, there is no known efficient approximation scheme. We show that the classical Spectra technique that is widely used in network reliability can be adapted for counting monotone CNF formulas. We prove that the proposed algorithm is logarithmically efficient for random monotone 2-CNF instances. Although we do not prove the efficiency of Spectra for k-CNF where k > 2, our experiments show that it is effective in practice for such formulas.

SUMMARY Proving the equivalence of successive, closely related versions of a program has the potential of being easier in practice than functional verification, although both problems are undecidable. There are three main reasons for this claim: (i) it circumvents the problem of specifying what the program should do; (ii) the problem can be naturally decomposed and hence is computationally easier; and (iii) there is an automatic invariant that enables to prove equivalence of loops and recursive functions in most practical cases. Theoretical and practical aspects of this problem are considered. Copyright © 2012 John Wiley & Sons, Ltd.

Coverage is an important measure for the quality and completeness of the functional verification of hardware logic designs. Verification teams spend a significant amount of time looking for bugs in the design and in providing high-quality coverage. This process is performed through the use of various sampling strategies for selecting test inputs. The selection of sampling strategies to achieve the verification goals is typically carried out in an intuitive manner. We studied several commonly used sampling strategies and provide a probabilistic framework for assessing and comparing their relative values. For this analysis, we derived results for two measures of interest: first, the probability of finding a bug within a given number of samplings; and second, the expected number of samplings until a bug is detected. These results are given for both recurring sampling schemes, in which the same inputs might be selected repeatedly, and for nonrecurring sampling schemes, in which already sampled inputs are never selected again. By considering results from the theory of search, and more specifically, from the well-known multiarmed bandit problem, we demonstrate the optimality of a greedy sampling strategy within our defined framework.

PCS is a CSP solver that can produce a machine-checkable deductive proof in case it decides that the input problem is unsatisfiable. The roots of the proof may be nonclausal constraints, whereas the rest of the proof is based on resolution of signed clauses, ending with the empty clause. PCS uses parameterized, constraint-specific inference rules in order to bridge between the nonclausal and the clausal parts of the proof. The consequent of each such rule is a signed clause that is 1) logically implied by the nonclausal premise, and 2) strong enough to be the premise of the consecutive proof steps. The resolution process itself is integrated in the learning mechanism, and can be seen as a generalization to CSP of a similar solution that is adopted by competitive SAT solvers.

Translation validation is a technique for formally establishing the semantic equivalence of the source and the target of a code generator. In this work we present a translation validation tool for the Real-Time Workshop code generator that receives as input Simulink models and generates optimized C code. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Proving the equivalence of successive, closely related versions of a program has the potential of being easier in practice than functional verification, although both problems are undecidable. There are two main reasons for this claim: it circumvents the problem of specifying what the program should do, and in many cases it is computationally easier. We study theoretical and practical aspects of this problem, which we call regression verification.

Boolean manipulation and existential quantification of numeric variables from linear arithmetic (LA) formulas is at the core of many program analysis and software model checking techniques (e.g., predicate abstraction). We present a new data structure, Linear Decision Diagrams (LDDs), to represent formulas in LA and its fragments, which has certain properties that make it efficient for such tasks. LDDs can be seen as an extension of Difference Decision Diagrams (DDDs) to full LA. Beyond this extension, we make three key contributions. First, we extend sifting-based dynamic variable ordering (DVO) from BDDs to LDDs. Second, we develop, implement, and evaluate several algorithms for existential quantification. Third, we implement LDDs inside CUDD, a state-of-the-art BDD package, and evaluate them on a large benchmark consisting of 850 functions derived from the source code of 25 open source programs. Overall, our experiments indicate that LDDs are an effective data structure for program analysis tasks.

Abstract We present a unifying framework for understanding and developing SAT-based decision procedures for Satisfiability Modulo Theories (SMT). The framework is based on a reduction of the decision problem to propositional logic by means of a deductive system. The two commonly used techniques, eager encodings (a direct reduction to propositional logic) and lazy encodings (a family of techniques based on an interplay between a SAT solver and a decision procedure) are identified as special cases. This framework offers the first generic approach for eager encodings, and a simple generalization of various lazy techniques that are found in the literature.

Given an LTL formula phi in negation normal form, it can be strengthened by replacing some of its literals with FALSE. Given such a formula and a model M that satisfies it, vacuity and mutual vacuity attempt to find one or a maximal set of literals, respectively, with which phi can be strengthened while still being satisfied by M. We study the problem of finding the strongest LTL formula that satisfies M and is in the Boolean closure of strengthened versions of phi as defined above. This formula is stronger or equally strong to any formula that can be obtained by vacuity and mutual vacuity. We present our algorithms in the framework of lattice automata.

We study the decision problem of disjunctive linear arithmetic over the reals from the perspective of computational geometry. We show that traversing the linear arrangement induced by the formula's predicates, rather than the DPLL(T) method of traversing the Boolean space, may have an advantage when the number of variables is smaller than the number of predicates (as it is indeed the case in the standard SMT-Lib benchmarks). We then continue by showing a branching heuristic that is based on approximating T-implications, based on a geometric analysis. We achieve modest improvement in run time comparing to the commonly used heuristic used by competitive solvers.

In formal verification, we verify that a system is correct with respect to a specification. Cases like antecedent failure can make a successful pass of the verification procedure meaningless. Vacuity detection can signal such "meaningless" passes of the specification, and indeed vacuity checks are now a standard component in many commercial model checkers. We address two dimensions of vacuity: the computational effort and the information that is given to the user. As for the first dimension, we present several preliminary vacuity checks that can be done without the design itself, which implies that some information can be found with a significantly smaller effort. As for the second dimension, we present algorithms for deriving three types of information that are not provided by standard vacuity checks, assuming M \= phi for a model M and property phi: a) behaviors that are possibly missing from M (or wrongly restricted by the environment) b) the largest subset of occurrences of literals in phi that can be replaced with false simultaneously without falsifying phi in M, and finally c) the degree of responsibility of each occurrence of a literal in phi to its satisfaction in the model M, which can be seen as a fine-grain form of vacuity. The complexity of each of these problems is proven. Overall this extra information can lead to tighter specifications and more guidance for finding errors.

This paper presents a procedure for the verification of multi-process systems based on considering a series of underapproximated models. The procedure checks models with an increasing set of allowed interleavings of the given set of processes, starting from a single interleaving. The procedure relies on SAT solvers' ability to produce proofs of unsatisfiability: from these proofs it derives information that guides the process of adding interleavings on the one hand, and determines termination on the other. The presented approach is integrated in a SAT-based Bounded Model Checking (BMC) framework. Thus, a BMC formulation of a multi-process system is introduced, which allows controlling which interleavings are considered. Preliminary experimental results demonstrate the practical impact of the presented method.

Separation Logic consists of a Boolean combination of predicates of the form v i ≥ v j + c where c is a constant and v i ,v j are variables of some ordered infinite type like real or integer. Any equality or inequality can be expressed in this logic. We propose a decision procedure for Separation Logic based on allocating small domains (ranges) to the formula’s variables that are sufficient for preserving satisfiability. Given a Separation Logic formula φ, our procedure constructs the inequalities graph of φ, based on φ’s predicates. This graph represents an abstraction of the formula, as there are many formulas with the same set of predicates. Our procedure then analyzes this graph and allocates a range to each variable that is adequate for all of these formulas. This approach of finding small finite ranges and enumerating them symbolically is both theoretically and empirically more efficient than methods based on case-splitting or reduction to Propositional Logic. Experimental results show that the state-space (that is, the number of assignments that need to be enumerated) allocated by our procedure is frequently exponentially smaller than previous methods.

When a program violates its specification a model checker produces a counterexample that shows an example of undesirable behavior. It is up to the user to understand the error, locate it, and fix the problem. Previous work introduced a technique for explaining and localizing errors based on finding the closest execution to a counterexample, with respect to a distance metric. That approach was applied only to concrete executions of programs. This paper extends and generalizes the approach by combining it with predicate abstraction. Using an abstract state-space increases scalability and makes explanations more informative. Differences between executions are presented in terms of predicates derived from the specification and program, rather than specific changes to variable values. Reasoning to the cause of an error from the factthat in the failing run x < y, but in the successful execution x = y is easier than reasoning from the information that in the failing run y = 239, but in the successful execution y = 232. An abstract explanation is automatically generalized

We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" counterexamples, i.e., traces that cannot be simulated on the original (concrete) machine. We check whether a counterexample is real or spurious with a satisfiability (SAT) checker. We then use a combination of 0-1 integer linear programming and machine learning techniques for refining the abstraction based on the counterexample. The process is repeated until either a real counterexample is found or the property is verified. We have implemented these techniques on top of the model checker NuSMV and the SAT solver Chaff. Experimental results prove the viability of these new techniques.

We describe new techniques for model checking in the counterexample guided abstraction/refinement framework. The abstraction phase ‘hides’ the logic of various variables, hence considering them as inputs. This type of abstraction may lead to ‘spurious’ counterexamples, i.e. traces that can not be simulated on the original (concrete) machine. We check whether a counterexample is real or spurious with a SAT checker. We then use a combination of Integer Linear Programming (ILP) and machine learning techniques for refining the abstraction based on the counterexample. The process is repeated until either a real counterexample is found or the property is verified. We have implemented these techniques on top of the model checker NuSMV and the SAT solver Chaff. Experimental results prove the viability of these new techniques. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.