| Vol-1889 urn:nbn:de:0074-1889-9 Copyright © 2017 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors.

# SMT 2017
Satisfiability Modulo Theories

### Proceedings of the 15th International Workshop on Satisfiability Modulo Theories
affiliated with the International Coference on Computer-Aided Verification (CAV 2017)

### Heidelberg, Germany, July 22 - 23, 2017.

Edited by

### Martin Brain *
Liana Hadarean **

* University of Oxford, Parks Rd, Oxford OX1 3QD, UK
** Synopsys, San Francisco, CA 94107, USA

## 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

2017-08-16: submitted by Liana Hadarean, metadata incl. bibliographic data published under Creative Commons CC0
2017-08-16: published on CEUR-WS.org |valid HTML5|