Saturday, July 22nd, 2017



09:00 - 10:00 Invited talk: Quantifier Instantiation Beyond E-Matching
Andrew Reynolds
10:00 - 10:30 Instantiation and Pretending to be an SMT Solver with Vampire
Giles Reger, Martin Suda and Andrei Voronkov

10:30 - 11:00 Coffee break

Session 1 (chair: Alberto Griggio)

11:00 - 11:30 OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing
Antti Hyvärinen, Matteo Marescotti, Leonardo Alt and Natasha Sharygina
11:30 - 12:00 Congruence Closure with Free Variables
Haniel Barbosa, Pascal Fontaine and Andrew Reynolds
12:00 - 12:30 Counterexample-Guided Model Synthesis
Mathias Preiner, Aina Niemetz and Armin Biere

12:30 - 14:00 Lunch

Session 2 (chair: Alexander Nadel)

14:00 - 14:30 Relational Constraint Solving in SMT
Baoluo Meng, Andrew Reynolds, Cesare Tinelli and Clark Barrett
14:30 - 15:00 Model-Based API Testing for SMT Solvers
Aina Niemetz, Mathias Preiner and Armin Biere
15:00 - 15:30 Visualising SMT-Based Parallel Constraint Solving
Jelena Budakovic, Matteo Marescotti, Antti Hyvärinen and Natasha Sharygina

15:30 - 16:00 Coffee break

Session 3 (chair: Bruno Dutertre)

16:00 - 16:30 Satisfiability Modulo Transcendental Functions via Incremental Linearization
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto Sebastiani
16:30 - 17:00 Generating Optimal Scheduling for Wireless Sensor Networks by Using Optimization Modulo Theories Solvers
Gergely Kovásznai, Csaba Biró and Balázs Erdélyi

Special session

17:00 onwards The Traditional SMT partial-functions discussion


     Sunday, July 23nd, 2017



09:00 - 10:00 Invited talk: SMT Nonlinear Real Arithmetic and Computer Algebra: a Dialogue of the Deaf?
James Davenport
10:00 - 10:30 Real Behavior of Floating Point
François Bobot, Zakaria Chihani and Bruno Marre

10:30 - 11:00 Coffee break

Session 4 (chair: Florian Schanda)

11:00 - 11:30 Subtropical Satisfiability
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm and Xuan Tung Vu
11:30 - 12:00 LibPoly: A Library for Reasoning about Polynomials
Dejan Jovanović and Bruno Dutertre
12:00 - 12:30 Z3str3: A String Solver with Theory-aware Branching
Murphy Berzish, Yunhui Zheng and Vijay Ganesh
12:30 - 14:00 Lunch

Session 5 (chair: Aina Niemetz)

14:00 - 14:20 An MCSAT treatment of Bit-Vectors
Stéphane Graham-Lengrand and Dejan Jovanović
14:20 - 14:40 Solving Constraints over Bit-Vectors with SAT-based Model Checking
Yakir Vizel, Alexander Nadel and Sharad Malik
14:40 - 15:00 Efficient Interpolation for the Theory of Arrays
Jochen Hoenicke and Tanja Schindler
15:00 - 15:30 SMT-COMP'17 Report

15:30 - 16:00 Coffee break

Session 6 (chair: Martin Brain)

16:00 - 17:00 SMT-LIB Updates and Discussion
17:00 - 17:30 Business Meeting

19:00 PC Dinner (location TBD)