SMT 2017
Satisfiability Modulo Theories

Table of Contents

• Preface
  
  

Invited Talks

• SMT Nonlinear Real Arithmetic and Computer Algebra: a Dialogue of the Deaf? 1
  James Davenport
• Quantifier Instantiation Beyond E-Matching 2
  Andrew Reynolds

Regular Papers

• Model-Based API Testing for SMT Solvers 3-14
  Aina Niemetz , Mathias Preiner , Armin Biere
• Generating Optimal Scheduling for Wireless Sensor Networks by Using Optimization Modulo Theories Solvers 15-27
  Gergely Kovasznai , Csaba Biro , Balazs Erdelyi
• LibPoly: A Library for Reasoning about Polynomials 28-39
  Dejan Jovanovic , Bruno Dutertre
• Visualising SMT-Based Parallel Constraint Solving 40-49
  Jelena Budakovic , Matteo Marescotti , Antti Hyvaerinen , Natasha Sharygina
• Real Behavior of Floating Point 50-62
  Francois Bobot , Zakaria Chihani , Bruno Marre
• Instantiation and Pretending to be an SMT Solver with Vampire 63-75
  Giles Reger , Martin Suda , Andrei Voronkov

Extended Abstracts

• Efficient Interpolation for the Theory of Arrays 76-88
  Jochen Hoenicke , Tanja Schindler
• An MCSAT treatment of Bit-Vectors 89-100
  Stephane Graham-Lengrand , Dejan Jovanovic
• Solving Constraints over Bit-Vectors with SAT-based Model Checking 101-107
  Yakir Vizel , Alexander Nadel , Sharad Malik

Presentation-only Papers

• Z3str3: A String Solver with Theory-aware Branching (paper published at FMCAD 2017, available here )
  Murphy Berzish , Yunhui Zheng , Vijay Ganesh
• Satisfiability Modulo Transcendental Functions via Incremental Linearization (paper published at CADE 2017, available here )
  Alessandro Cimatti , Alberto Griggio , Ahmed Irfan , Marco Roveri , Roberto Sebastiani
• Congruence Closure with Free Variables (paper published at TACAS 2017, available here )
  Haniel Barbosa , Pascal Fontaine , Andrew Reynolds
• Relational Constraint Solving in SMT (paper published at CADE 2017, available here )
  Baoluo Meng , Andrew Reynolds , Cesare Tinelli , Clark Barrett
• Subtropical Satisfiability (paper published at FroCoS 2017, available here )
  Pascal Fontaine , Mizuhito Ogawa , Thomas Sturm , Xuan Tung Vu
• Counterexample-Guided Model Synthesis (paper published at TACAS 2017, available here )
  Mathias Preiner , Aina Niemetz , Armin Biere
• OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing (paper published at SAT 2016, available here )
  Antti Hyvaerinen , Matteo Marescotti , Leonardo Alt , Natasha Sharygina