View: session overviewtalk overviewside by side with other conferences
08:45  LaSh and QUANTIFY Openings SPEAKER: Lash 
09:00  Instantiationbased reasoning, EPR encodings and all that SPEAKER: Konstantin Korovin ABSTRACT. Instantiationbased reasoning aims to combine the expressivity of firstorder logic with the efficiency of propositional and SMT reasoning. Most instantiation based methods are complete for firstorder logic and are especially efficient for the effectively propositional fragment (EPR). It turns out that many problems such as model checking, bitvector reasoning, finite model finding and QBF solving can be succinctly encoded into the EPR fragment. In this talk I will discuss recent developments in instantiationbased reasoning, EPR based encodings and related challenges.

10:45  Quantifier handling in calculi for quantified Boolean formulas SPEAKER: Uwe Egly ABSTRACT. Quantified Boolean formulas (QBFs) generalize propositional formulas 
11:30  Encoding Reachability with Quantification SPEAKER: Michael Cashmore ABSTRACT. We report on techniques for translating bounded propositional reachability problems into Quantified Boolean Formulae (QBF). The techniques exploit the binarytree structure of the QBF quantification to produce encodings logarithmic in the size of the instance and thus exponentially smaller than the corresponding SAT encoding with the same bound. We briefly describe our experimental results, and discuss the challenging structure that is implicit in these encodings. 
12:00  EPR Encodings of BitVector Problems Even With Quantifiers SPEAKER: Gergely Kovásznai ABSTRACT. Bitprecise reasoning is essential in many applications of Satisfiability Modulo Theories (SMT). Quantifierfree resp. quantified bitvector formulas (QF_BV resp. BV) play an important role in hardware resp. software verification. In recent years, efficient approaches for solving such formulas have been developed. Most of the QF_BV solvers rely on bitblasting, while BV solvers rely on quantifier instantiation. In [Kovasznai, Froehlich, & Biere, SMT 2012], we investigated the worstcase complexity of those logics and argued that bitblasting resp. quantifier instantiation is exponential resp. doubleexponential in general. We also introduced the criterion "bitwidth boundedness" to bitvector problems, as a property that seems to hold for most practical problems, and proved it to reduce the worstcase complexity by an exponential. 
12:30  Beyond QResolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction SPEAKER: Hubie Chen ABSTRACT. We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a firstorder sentence (not assumed here to be in prenex form) built from conjunction and quantification, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Qresolution proof system in a broader context; we will discuss how, in a sense made precise, it generalizes Qresolution and gives a clear proof of the soundness of Qresolution.
As an application, we give an algebraic, EhrenfeuchtFraïsséstyle characterization of the condition of not having boundedwidth proofs (for a QCSP instance) and show that the resulting theory can be used to obtain tractability results for the QCSP.
This talk is based on the article available at http://arxiv.org/abs/1403.0222. 
14:30  Algorithmic Paradigms for Solving QBF SPEAKER: Fahiem Bacchus ABSTRACT. The past 15 years has seen tremendous improvement in the effectiveness of solvers for Quantified Boolean Formulas (QBF). This talk will discuss some of the main algorithmic approaches that have been employed in constructing such solvers. We will aim to identify certain features of these approaches that are effective and not so effective. Some of the theoretical questions that arise from our empirical experience with these solvers will be identified in an attempt to spur more synergy between theory and practice for solving QBF. 
15:30  Projective Quantifier Elimination for Equational Constraint Solving SPEAKER: Paqui Lucio ABSTRACT. We deal with (general) equational constraints, that is, firstorder formulas, with equality as its only predicate symbol, over a (finite or infinite) language $\Language$ of function symbols. As semantic domain, we consider the algebra of finite terms over L. Solving one of such constraints means to find all the solutions for (i.e. assignments to) its free variables. We present the Projective Quantifier Elimination (PQE) technique for solving equational constraints (in particular, deciding their satisfiability) that performs an algebraicstyle transformation of expressions instead of handling firstorder formulas. PQE is formulated on the basis of three algebraic operations on expressions: complement, intersection and projection. We aim to contribute not only a new style of quantifier elimination for constraint solving, but also a more efficient method for equational constraint solving. PQE avoids unnecessary applications of the costly Explosion Rule (ER) that are performed by traditional solving methods. 
16:30  Efficiently Solving Quantified BitVectors SPEAKER: Christoph Wintersteiger ABSTRACT. There is great interest in the use of symbolic reasoning for synthesising loop invariants, ranking functions, or whole program fragments and hardware circuits. Solvers for the quantifierfree fragment of bitvector logic exist and often rely on SAT solvers for efficiency. However, many techniques require quantifiers in bitvector formulas to avoid an exponential blowup during construction and QBF solvers are often inefficient. I will present an approach based on a set of effective wordlevel simplifications that are traditionally employed in automated theorem proving, heuristic quantifier instantiation methods used in SMT solvers, and model finding techniques based on function templates. I will also go into why we got interested in this problem in the first place and where we would like to take it from here. 
17:00  Quantifier Projection SPEAKER: Nikolaj Bjorner ABSTRACT. We take as starting point routines for quantifier reasoning in the SMT solver Z3 and we analyze these through the lens of quantfier projection: quantifiers are specialized or instantiated partially using information about possible feasible interpretations that is collected during search. 
17:30  Finding Conflicting Instances of Quantified Formulas in SMT SPEAKER: Andrew Reynolds ABSTRACT. Modern SMT solvers primarily rely on heuristic methods such as Ematching for answering ``unsatisfiable" in the presence of quantified formulas. The success of these solvers is often hindered by an overabundance of instantiations produced by these heuristics, making it difficult for the solver to continue its operation. In this paper, we introduce new techniques that alleviate this shortcoming by first discovering instantiations that are in conflict with the current state of the solver. In these techniques, the solver only resorts to heuristic methods when such an instantiation cannot be found, thus decreasing its dependence upon Ematching. Our experimental results show our technique significantly reduces the number of instantiations required by the SMT solver for answering ``unsatisfiable" for several benchmark libraries, and consequently leads to improvements over stateoftheart implementations. 