Craig interpolation has turned out to be an essential method for many applications in formal verification. In this paper we focus on the computation of simple interpolants for the theory of linear arithmetic with rational coefficients. We successfully minimize the number of linear constraints in the final interpolant by several methods including proof transformations, linear programming, and SMT solving. Experimental results comparing the approach to standard methods from the literature prove the effectiveness of the approach and show reductions of up to 70% in the number of linear constraints.

Craig interpolation has become a powerful and universal tool in the formal verification domain, where it is used not only for Boolean systems, but also for timed systems, hybrid systems, and software programs. The latter systems demand interpolation for fragments of first-order logic. When it comes to model checking, the structural compactness of interpolants is necessary for efficient algorithms. In this paper, we present a method to reduce the size of interpolants derived from proofs of unsatisfiability produced by SMT (Satisfiability Modulo Theory) solvers. Our novel method uses structural arguments to modify the proof in a way, that the resulting interpolant is guaranteed to have smaller size. To show the effectiveness of our approach, we apply it to an extensive set of formulas from symbolic hybrid model checking.

In this paper we present a method for integrating two complementary solving techniques for QBF formulas, i.e. variable elimination based on an AIG-framework and search with DPLL based solving. We develop a sophisticated mechanism for coupling these techniques, enabling the transfer of partial results from the variable elimination part to the search part. This includes the definition of heuristics to (1) determine appropriate points in time to snapshot the current partial result during variable elimination (by estimating its quality) and (2) switch from variable elimination to search-based methods (applied to the best known snapshot) when the progress of variable elimination is supposed to be too slow or when representation sizes grow too fast. We will show in the experimental section that our combined approach is clearly superior to both individual methods run in a stand-alone manner. Moreover, our combined approach significantly outperforms all other state-of-the-art solvers.

In this paper we present a solver for Quantified Boolean Formulas (QBFs) which is based on And-Inverter Graphs (AIGs). We use a new quantifier elimination method for AIGs, which heuristically combines cofactor-based quantifier elimination with quantification using BDDs and thus benefits from the strengths of both data structures. Moreover, we present a novel SAT-based method for preprocessing QBFs that is able to efficiently detect variables with forced truth assignments, allowing for an elimination of these variables from the input formula. We describe the used algorithm which heavily relies on the incremental features of modern SAT-solvers. Experimental results demonstrate that our preprocessing method can significantly improve the performance of QBF preprocessing and thus is able to accelerate the overall solving process when used in combination with state-of-the-art QBF-solvers. In particular, we integrated the preprocessing technique as well as the quantifier elimination method into the QBF-solver AIGSolve, allowing it to outperform state-of-the-art solvers.

In this paper we present a procedure for solving quantified boolean formulas (QBF), which uses And-Inverter Graphs (AIGs) as the core data-structure. We make extensive use of structural information extracted from the input formula such as functional definitions of variables and non-linear quantifier structures. We show how this information can directly be exploited by the symbolic, AIG based representation. We implemented a prototype QBF solver based on our ideas and performed a number of experiments proving the effectiveness of our approach, and moreover, showing that our method is able to solve QBF instances on which state-of-the-art QBF solvers known from literature fail.

In this paper we present a complete method for verifying properties expressed in the temporal logic CTL. In contrast to the majority of verification methods presented in previous years, we support unbounded model checking based on symbolic representations of characteristic functions. Among others, our method is based on an advanced and-inverter graph (AIG) implementation, quantifier scheduling, and BDD sweeping. For several examples, our method outperforms BDD based symbolic model checking by orders of magnitude. However, our approach is also able to produce competitive results for cases where BDD are known to perform well