SMT Program

SMT PROGRAM

Days: Thursday, July 12th Friday, July 13th

Thursday, July 12th

View this program: with abstracts session overview talk overview side by side with other conferences

Chair:

Location: Green Templeton Lecture Theatre

09:00	Thomas Wies Invited talk: Automating Separation Logics using SMT (abstract)
10:00	Andrew Reynolds, Haniel Barbosa and Pascal Fontaine Revisiting Enumerative Instantiation (abstract)

10:30-11:00Coffee Break

11:00-12:30 Session 74F

Chair:

Aina Niemetz

Location: Green Templeton Lecture Theatre

11:00	Martin Brain, Florian Schanda and Youcheng Sun Building Better Bit-Blasting for Floating-Point Problems (abstract)
11:30	Peter Backeman, Aleksandar Zeljić, Philipp Ruemmer and Christoph M. Wintersteiger The next 10^4 UppSAT Approximations (abstract)
12:00	Mohamed Iguernlala, Sylvain Conchon and Albin Coquereau Alt-Ergo 2.2 (abstract)

12:30-14:00Lunch Break

14:00-15:30 Session 76H

Location: Green Templeton Lecture Theatre

14:00	Krishnamurthy Dvijotham Invited talk: Verifying Learners and Learning Verifiers (abstract)
15:00	Gergely Kovásznai, Csaba Biró and Balázs Erdélyi Puli - A Problem-Specific OMT Solver (abstract)

15:30-16:00Coffee Break

16:00-17:30 Session 78E

Chair:

Philipp Ruemmer

Location: Green Templeton Lecture Theatre

16:00	Leonardo Alt and Christian Reitwiessner SMT-based Compile-time Verification of Safety Properties for Smart Contracts (abstract)
16:30	Guillaume Bury, David Delahaye and Simon Cruanes SMT Solving Modulo Tableau and Rewriting Theories (abstract)
17:00	Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Noetzli, Mathias Preiner, Clark Barrett and Cesare Tinelli Rewrites for SMT Solvers using Syntax-Guided Enumeration (abstract)

Friday, July 13th

View this program: with abstracts session overview talk overview side by side with other conferences

09:00-10:30 Session 83J

Chair:

Vijay D'Silva

Location: Green Templeton Lecture Theatre

09:00	Christoph Benzmüller 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 (abstract)
10:00	Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui and Cesare Tinelli Higher-Order SMT Solving (abstract)

10:30-11:00Coffee Break

11:00-12:30 Session 86K

Chair:

Alexander Nadel

Location: Green Templeton Lecture Theatre

11:00	François Bobot, Stephane Graham-Lengrand, Bruno Marre and Guillaume Bury Centralizing Equality Reasoning in MCSAT (abstract)
11:30	Maria Paola Bonacina, Stéphane Graham-Lengrand and Natarajan Shankar Proofs in conflict-driven theory combination (abstract)
12:00	Tanja Schindler and Dejan Jovanović Selfless Interpolation for Infinite-State Model Checking (abstract)

12:30-14:00Lunch Break

14:00-15:30 Session 87K

Chair:

Andrew Reynolds

Location: Green Templeton Lecture Theatre

14:00	Arie Gurfinkel, Sharon Shoham and Yakir Vizel Discovering Universally Quantified Solutions for Constrained Horn Clauses (abstract)
14:30	Giles Reger and Martin Riener What is the Point of an SMT-LIB Problem? (abstract)
15:00	Smt-Comp Organizers SMT-COMP 2018 Report (abstract)

15:30-16:00Coffee Break

16:00-17:30 Session 88H: SMT-LIB Updates and Discussion

Chair:

Cesare Tinelli

Location: Green Templeton Lecture Theatre

17:30-18:00 Session 92: SMT Business meeting

Chair:

Clark Barrett

Location: Green Templeton Lecture Theatre

19:00-21:30 Workshops dinner at Keble College

Workshops dinner at Keble College. Drinks reception from 7pm, to be seated by 7:30 (pre-booking via FLoC registration system required; guests welcome).

Location: Keble College