Accepted Papers and Presentations

Regular Talks

  • Alexander Nadel and Nachum Dershowitz
    Is Bit-Vector Reasoning as Hard as NExpTime in Practice? [pdf]
  • Marco Gario and Andrea Micheli
    PySMT: a Solver-Agnostic Library for Fast Prototyping of SMT-Based Algorithms [pdf]
  • Richard Bonichon, David Déharbe, Pablo Federico Dobal and Cláudia Tavares
    SMTpp: preprocessors and analyzers for SMT-LIB [pdf]
  • Kshitij Bansal, Eric Koskinen and Omer Tripp [Moved to EC2]
    Synthesis of Commutativity Conditions
  • Andrew Reynolds, Jasmin Blanchette and Cesare Tinelli
    Model Finding for Recursive Functions in SMT [pdf]
  • Yasser Shoukry, Pierluigi Nuzzo, Alberto Puggelli, Alberto Sangiovanni-Vincentelli, Sanjit Seshia, Mani Srivastava and Paulo Tabuada
    Imhotep-SMT: A Satisfiability Modulo Theory Solver For Secure State Estimation [pdf]
  • Andreas Fellner, Pascal Fontaine, Georg Hofferek and Bruno Woltzenlogel Paleo
    NP-completeness of small conflict set generation for congruence closure [pdf]
  • Joe Hendrix and Ben Jones
    Bounded Integer Linear Constraint Solving via Lattice Search [pdf]
  • Liana Hadarean, Alex Horn and Tim King
    A Concurrency Problem with Exponential DPLL(T) Proofs [pdf]
  • Stéphane Graham-Lengrand
    Slot Machines: an approach to the Strategy Challenge in SMT solving
  • Bruno Dutertre
    Solving Exists/Forall Problems With Yices [pdf]
  • Sam Bayless, Noah Bayless, Holger Hoos and Alan J. Hu
    SAT Modulo Monotonic Theories
  • Liana Hadarean, Ruben Martins, Martin Brain and Daniel Kroening
    Stronger, Better, Faster: Optimally Propagating SAT Encodings
  • Martin Bromberger, Thomas Sturm and Christoph Weidenbach
    Linear Integer Arithmetic Revisited

Invited talks

Cristian Cadar, Imperial College London
Constraint Solving in Symbolic Execution

Constraint solving plays a key role in symbolic execution, an effective and popular technique for testing complex software. In this talk, I will give an overview of symbolic execution, and I will discuss the constraint solving challenges arising in applying symbolic execution to several application domains, including whole-program bug-finding, high-coverage patch testing, testing and verification of performance optimisations, and recovery of broken documents without any prior knowledge of the file format.

Margus Veanes, Microsoft Research
Strings and Automata Modulo Theories

Analysis of string manipulating programs is relevant in many different domains.  In real applications, characters in strings often range over Unicode and are usually treated as bit-vectors. In that sense, the theory of strings is really parametric in the theory of characters. This poses a unique challenge in integrating it as a theory into existing SMT solvers. Rather than integrating the theory of strings into an SMT solver, the focus of this talk is to illustrate how one can integrate an SMT solver into a domain specific tool for reasoning about strings. We focus on domain specific languages and tasks that admit automata or transducer based formulations, such as regexes, and specialized languages for string sanitizers, string encoders, and string decoders. Many analysis problems over strings that can be formulated through automata or transducer based algorithms become scalable through extensions based on using an SMT solver. Such algorithm extensions also pose new challenges in the automata community.

John Regehr, University of Utah
Compiler Optimizations and SMT

We are using SMT to verify existing compiler optimizations in LLVM and also to find missing ones. The automation provided by solvers has been instrumental in mechanizing the semantics of LLVM code, and in particular its undefined behaviors, which are not very well understood. We have found a number of incorrect optimizations and have used synthesis to identify many missing ones. This talk will present some of our results and will discuss several areas where we, so far, have not had good luck getting solvers to work for us.