Accepted Papers

Regular Papers

Model-Based API Testing for SMT Solvers (paper)
Aina Niemetz, Mathias Preiner and Armin Biere

Generating Optimal Scheduling for Wireless Sensor Networks by Using Optimization Modulo Theories Solvers (paper)
Gergely Kovásznai, Csaba Biró and Balázs Erdélyi

LibPoly: A Library for Reasoning about Polynomials (paper)
Dejan Jovanović and Bruno Dutertre

Visualising SMT-Based Parallel Constraint Solving (paper)
Jelena Budakovic, Matteo Marescotti, Antti Hyvärinen and Natasha Sharygina

Real Behavior of Floating Point (paper)
François Bobot, Zakaria Chihani and Bruno Marre

Instantiation and Pretending to be an SMT Solver with Vampire (paper)
Giles Reger, Martin Suda and Andrei Voronkov

Extended Abstracts

Efficient Interpolation for the Theory of Arrays (paper)
Jochen Hoenicke and Tanja Schindler

An MCSAT treatment of Bit-Vectors (paper)
Stéphane Graham-Lengrand and Dejan Jovanović

Solving Constraints over Bit-Vectors with SAT-based Model Checking (paper)
Yakir Vizel, Alexander Nadel and Sharad Malik

Presentation-only Papers

Z3str3: A String Solver with Theory-aware Branching
Murphy Berzish, Yunhui Zheng and Vijay Ganesh

Satisfiability Modulo Transcendental Functions via Incremental Linearization
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto Sebastiani

Congruence Closure with Free Variables
Haniel Barbosa, Pascal Fontaine and Andrew Reynolds

Relational Constraint Solving in SMT
Baoluo Meng, Andrew Reynolds, Cesare Tinelli and Clark Barrett

Subtropical Satisfiability
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm and Xuan Tung Vu

Counterexample-Guided Model Synthesis
Mathias Preiner, Aina Niemetz and Armin Biere

OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing
Antti Hyvärinen, Matteo Marescotti, Leonardo Alt and Natasha Sharygina