July 12th, 2018
Session 1 | |
| 09:00 - 10:00 | Invited talk: Automating Separation Logics using SMT
Thomas Wies |
| 10:00 - 10:30 | Revisiting Enumerative Instantiation
Andrew Reynolds, Haniel Barbosa and Pascal Fontaine |
| 10:30 - 11:00 | Coffee break |
Session 2 | |
| 11:00 - 11:30 | Building Better Bit-Blasting for Floating-Point Problems
Martin Brain, Florian Schanda and Youcheng Sun |
| 11:30 - 12:00 | The next 10^4 UppSAT Approximations
Peter Backeman, Aleksandar Zeljić, Philipp Ruemmer and Christoph M. Wintersteiger |
| 12:00 - 12:30 | Alt-Ergo 2.2
Mohamed Iguernlala, Sylvain Conchon and Albin Coquereau |
| 12:30 - 14:00 | Lunch |
Session 3 | |
| 14:00 - 15:00 | Invited talk: Verifying Learners and Learning Verifiers
Krishnamurthy Dvijotham |
| 15:00 - 15:30 | Puli - A Problem-Specific OMT Solver
Gergely Kovásznai, Csaba Biró and Balázs Erdélyi |
| 15:30 - 16:00 | Coffee break |
Session 4 | |
| 16:00 - 16:30 | SMT-based Compile-time Verification of Safety Properties for Smart Contracts
Leonardo Alt and Christian Reitwiessner |
| 16:30 - 17:00 | SMT Solving Modulo Tableau and Rewriting Theories
Guillaume Bury, David Delahaye and Simon Cruanes |
| 17:00 -17:30 | Rewrites for SMT Solvers using Syntax-Guided Enumeration
Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Noetzli, Mathias Preiner, Clark Barrett and Cesare Tinelli |
July 13th, 2018
Session 5 | |
| 09:00 - 10:00 | Invited talk: Experiments in Universal Logical Reasoning --- How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic
Christoph Benzmüller |
| 10:00 - 10:30 | Higher-Order SMT Solving
Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui and Cesare Tinelli |
| 10:30 - 11:00 | Coffee break |
Session 6 | |
| 11:00 - 11:30 | Centralizing Equality Reasoning in MCSAT
François Bobot, Stephane Graham-Lengrand, Bruno Marre and Guillaume Bury |
| 11:30 - 12:00 | Proofs in conflict-driven theory combination
Maria Paola Bonacina, Stéphane Graham-Lengrand and Natarajan Shankar |
| 12:00 - 12:30 | Selfless Interpolation for Infinite-State Model Checking
Tanja Schindler and Dejan Jovanović |
| 12:30 - 14:00 | Lunch |
Session 7 | |
| 14:00 - 14:30 | Discovering Universally Quantified Solutions for Constrained Horn Clauses
Arie Gurfinkel, Sharon Shoham and Yakir Vizel |
| 14:30 - 15:00 | What is the Point of an SMT-LIB Problem?
Giles Reger and Martin Riener |
| 15:00 - 15:30 | SMT-COMP 2018 Report |
| 15:30 - 16:00 | Coffee break |
Session 8 | |
| 16:00 - 17:30 | SMT-LIB Updates and Discussion |
| 17:30 - 18:00 | Business Meeting |