View: session overviewtalk overview

10:30 | Better Lemmas with Lambda Extraction SPEAKER: unknown 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. |

11:00 | A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas SPEAKER: unknown 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. |

11:30 | CAQE: A Certifying QBF Solver SPEAKER: unknown 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. |

12:00 | Universal Boolean Functional Vectors SPEAKER: Jesse Bingham 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. |