Saturday, July 22nd, 2017
| 09:00 - 10:00 | Invited talk: Quantifier Instantiation Beyond E-Matching
(slides) Andrew Reynolds |
| 10:00 - 10:30 | Instantiation and Pretending to be an SMT Solver with Vampire
(slides) 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
(slides) Antti Hyvärinen, Matteo Marescotti, Leonardo Alt and Natasha Sharygina |
| 11:30 - 12:00 | Congruence Closure with Free Variables
(slides) Haniel Barbosa, Pascal Fontaine and Andrew Reynolds |
| 12:00 - 12:30 | Counterexample-Guided Model Synthesis
(slides) 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
(slides) Aina Niemetz, Mathias Preiner and Armin Biere |
| 15:00 - 15:30 | Visualising SMT-Based Parallel Constraint Solving
(slides) 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
(slides) 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
(slides)
Gergely Kovásznai, Csaba Biró and Balázs Erdélyi |
Special session | |
| 17:00 onwards | The Traditional SMT partial-functions discussion (slides) |
Sunday, July 23nd, 2017
| 09:00 - 10:00 | Invited talk: SMT Nonlinear Real Arithmetic and Computer Algebra: a Dialogue of the Deaf?
(slides) James Davenport |
| 10:00 - 10:30 | Real Behavior of Floating Point
(slides) 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
(slides) Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm and Xuan Tung Vu |
| 11:30 - 12:00 | LibPoly: A Library for Reasoning about Polynomials
(slides Intro Table CAD)
Dejan Jovanović and Bruno Dutertre |
| 12:00 - 12:30 | Z3str3: A String Solver with Theory-aware Branching
(slides) 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
(slides)
Stéphane Graham-Lengrand and Dejan Jovanović |
| 14:20 - 14:40 | Solving Constraints over Bit-Vectors with SAT-based Model Checking
(slides) Yakir Vizel, Alexander Nadel and Sharad Malik |
| 14:40 - 15:00 | Efficient Interpolation for the Theory of Arrays
(slides) 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) |