| Vol-1617 urn:nbn:de:0074-1617-8 Copyright © 2016 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 2016
Satisfiability Modulo Theories

### Proceedings of the 14th International Workshop on Satisfiability Modulo Theories
affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)

### Coimbra, Portugal, July 1 - 2, 2016.

Edited by

### Tim King *
Ruzica Piskac **

* Google, Inc., Mountain View, CA 94043, USA
** Computer Science Department, Yale University, New Haven, CT 06511, USA

## Table of Contents

- Preface

### Invited Talks

- The Nuts and Bolts of Yices 1
  Bruno Dutertre
- SMT Techniques and Solvers in Automated Termination Analysis 2
  Carsten Fuhs
- Constraint Programming - an Introduction, with some Applications to String Processing 3
  Justin Pearson

### Regular Papers

- Kneecap: Model-based Generation of Network Traffic 4-14
  Nik Sultana, Richard Mortier
- Computing a Complete Basis for Equalities Implied by a System of LRA Constraints 15-30
  Martin Bromberger, Christoph Weidenbach
- Scrambling and Descrambling SMT-LIB Benchmarks 31-40
  Tjark Weber
- Algebraic Polynomial-based Synthesis for Abstract Boolean Network Analysis 41-50
  Peter Backeman, Christoph M. Wintersteiger, Boyan Yordanov, Sara-Jane Dunn
- LOIS: an Application of SMT Solvers 51-60
  Eryk Kopczynski, Szymon Toruńczyk

### Extended Abstracts

- Reasoning with Sets and Sums of Sets 61-70
  Markus Bender
- Satisfiability Modulo Free Data Structures Combined with Bridging Functions 71-80
  Raphael Berthon, Christophe Ringeissen
- On Intervals and Bounds in Bit-vector Arithmetic 81-84
  Mikolas Janota, Christoph M. Wintersteiger
- On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT 85-95
  Roberto Sebastiani, Patrick Trentin

### Presentation-only Papers

- Clause Sharing and Partitioning for Cloud-Based SMT Solving (paper published at ATVA 2016, available here)
  Matteo Marescotti, Antti Hyvärinen, Natasha Sharygina
- Deciding Bit-Vector Formulas with mcSAT (paper published at SAT 2016, available here)
  Aleksandar Zeljić, Christoph M. Wintersteiger, Philipp Ruemmer
- Z3str2+BV: A Solver for a Theory of Strings and Bit-vectors (Z3str2 solver, paper available here)
  Murphy Berzish, Sanu Subramanian, Yunhui Zheng, Omer Tripp, Vijay Ganesh
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures (The MathCheck2 web site)
  Curtis Bright, Vijay Ganesh, Albert Heinle, Ilias Kotsireas, Saeed Nejati, Krzysztof Czarnecki
- Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers (paper published at SAT 2016, available here)
  Jeevana Priya Inala, Rohit Singh, Armando Solar-Lezamah
- Proof Certificates for SMT-based Model Checkers
  Alain Mebsout, Cesare Tinelli

2016-06-30: submitted by Ruzica Piskac, metadata incl. bibliographic data published under Creative Commons CC0
2016-06-30: published on CEUR-WS.org |valid HTML5|