ABSTRACT. In Satisfiability Modulo Theories (SMT), the theory of arrays provides operations to access and modify an array at a given index, e.g., read and write. However, common operations to modify multiple indices at once, e.g., memset or memcpy of the standard C library, are not supported. We describe algorithms to identify and extract array patterns representing such operations, including memset and memcpy. We represent these patterns in our SMT solver Boolector by means of compact and succinct lambda terms, which yields better lemmas and increases overall performance. We describe how extraction and merging of lambda terms affects lemma generation, and provide an extensive experimental evaluation of the presented techniques. It shows a considerable improvement in terms of solver performance, particularly on instances from symbolic execution.

ABSTRACT. Given an existentially quantified formula \exists x_1 ... x_n \phi, a Skolem function vector for x_1, ... x_n is a vector of functions F_1, ... F_n such that substituting F_i for x_i in \phi for all i in 1 through n gives a formula semantically equivalent to \exists x_1 ... x_n \phi(x_1 , ..., x_n). Automatically generating Skolem function vectors is of significant interest in several applications including certified QBF solving, finding strategies of players in games, synthesising circuits and bit-vector programs from specifications, disjunctive decomposition of sequential circuits and the like. In many applications, \phi is given as a conjunction of propositional factors, each of which depends on a small subset of variables. Existing algorithms for Skolem function generation ignore any such factored form and treat \phi as a monolithic function. This presents scalability hurdles in medium to large problem instances. In this paper, we argue that exploiting the factored form of \phi can give significant performance improvements in practice when computing Skolem functions. We present a CEGAR style algorithm for generating Skolem functions for factored propositional formulas. In contrast to other algorithms in the literature, our algorithm neither requires proof of satisfiability of a QBF formula nor uses composition of monolithic conjunctions of factors. We show experimentally that our algorithm can generate smaller Skolem functions and works better on larger benchmarks than state-of- the-art composition based techniques.

ABSTRACT. We present a new CEGAR-based algorithm for QBF. The algorithm builds on a decomposition of QBFs into a sequence of propositional formulas, which we call the clausal abstraction. For each quantifier level we create a propositional formula that contains only the variables of the quantifier level and some additional variables describing the interaction with adjacent quantifier levels. This leads to a simplified notion of refinement for CEGAR-based QBF algorithms. Experimental results with our implementation CAQE show that we outperform current QBF solvers in benchmarks with many quantifier alternations.

Furthermore, we show how to effectively construct Skolem and Herbrand functions from true, respectively false, QBFs; allowing us to certify the solver result. Our solver is able to certify significantly more results than previous methods.

ABSTRACT. Typically, one represents a boolean function using expressions over variables, where each variable corresponds to a function input. So-called \emph{parametric representations}, used to represent a function in some restricted sub-space of its domain, break this correspondence by allowing inputs to be associated with \emph{functions}. This can lead to more succinct representations, for example when using binary decision diagrams (BDDs). Here we introduce \emph{Universal Boolean Functional Vectors} (UBFV), which also break the correspondence, but done so such that all input vectors are accounted for. Intelligent choice of a UBFV can have a dramatic impact on BDD size; for instance we show how the \emph{hidden weighted bit function} can be efficiently represented using UBFVs (whereas without UBFVs, BDDs are known to be exponential for any variable order). We show several industrial examples where the UBFV approach has a huge impact on proof performance, the ``killer app'' being floating point addition, wherein the wide case split used in the state-of-the-art approach is entirely done away with, resulting in 20x reduction in proof runtime. We give other theoretical and experimental results, and also provide two approaches to verifying the crucial ``universality'' aspect of a proposed UBFV. Finally, we suggest several interesting avenues of future research stemming from this program.

ABSTRACT. IC3 is undoubtedly one of the most successful and important recent techniques for unbounded model checking. Understanding and improving IC3 has been a subject of a lot of recent research. In this regard, the most fundamental questions are how to choose Counterexamples to Induction (CTIs) and how to generalize them into (blocking) lemmas. Answers to both questions influence performance of the algorithm by directly affecting the quality of the lemmas learned. In this paper, we present a new IC3-based algorithm, called QUIP (QUIP is an acronym for ``a QUest for an Inductive Proof''), that is designed to more aggressively propagate (or push) learned lemmas to obtain a safe inductive invariant faster. QUIP modifies the recursive blocking procedure of IC3 to prioritize pushing already discovered lemmas over learning of new ones. However, a naive implementation of this strategy floods the algorithm with too many useless lemmas. In QUIP, we solve this by extending IC3 with may-proof-obligations (corresponding to the negations of learned lemmas), and by using an under-approximation of reachable states (i.e., states that witness why a may-proof-obligation is satisfiable) to prune non-inductive lemmas. We have implemented QUIP on top of an industrial-strength implementation of IC3. The experimental evaluation on HWMCC benchmarks shows that the QUIP is a significant improvement (at least 2x in runtime and more properties solved) over IC3. Furthermore, the new reasoning capabilities of QUIP naturally lead to additional optimizations and new techniques that can lead to further improvements in the future.

ABSTRACT. In recent years, the inductive, incremental verification algorithm IC3 had a major impact on hardware model checking. Also with respect to software model checking, a number of adaptations of Boolean IC3 and combinations with CEGAR and ART-based techniques have been developed. However, most of them exploit the peculiarities of software programs, such as the explicit representation of control flow, only to a limited extent. In this paper, we propose a technique that supports this explicit representation in the form of control flow automata, and integrates it with symbolic reasoning about the data state space of the program. It thus provides a true lifting of IC3 from hardware to software model checking. By evaluating the approach on a number of case studies using a prototypical implementation, we demonstrate that our method shows promising results.

ABSTRACT. In the early phases of the design of safety-critical systems, we need the ability to analyze the safety of different design solutions, comparing how different functional allocations impact on the overall reliability of the system. To achieve this goal, we can apply formal techniques ranging from model checking to model-based fault-tree analysis. By using the results of the verification and safety analysis, we can compare the different solutions and provide the domain experts with information on the strengths and weaknesses of each solution.

In this paper, we consider NASA's early designs and functional allocation hypotheses for the next air traffic control system for the United States. In particular, we consider how the allocation of separation assurance capabilities and the required communication between agents affects the safety of the overall system. Due to the high level of details, we need to abstract the domain while retaining all of the key properties of NASA's designs. We present the modeling approach and verification process that we adopted. Finally, we discuss the results of the analysis when comparing different configurations including both new, self-separating and traditional, ground-separated aircraft.

ABSTRACT. Model checking has become a formal sign-off requirement in the verification plans of many hardware designs. For design sizes encountered in practice, compositional assume-guarantee reasoning is often necessary to achieve satisfactory results. However, many pitfalls exist that can create unsound or unexpected results for users of commercial model checking tools. Users need to watch out for circularity in properties, for dead-ends getting trimmed by tools, as well as understand the differences in proof composition for liveness and safety properties. We present many real design examples to illustrate these points, as well as describe our experiences with compositional reasoning in practice.