MONDAY June 27:

09:15--09:30  Opening
09:30--10:30  Invited Talk
 Sumit Gulwani.  Programming by Examples: Applications, Algorithms, and Ambiguity Resolution

10:30--11:00  Break

11:00--12:00  Session Satisfiability of Boolean Formulas

11:00--11:30
 Benjamin Kiesl, Martina Seidl, Hans Tompits and Armin Biere. Super-Blocked Clauses
11:30--12:00
 Jasmin Christian Blanchette, Mathias Fleury and Christoph Weidenbach. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

12:00--14:00  Lunch

14:00--15:40  Session First-Order Theorem Proving

14:00--14:30
 Giles Reger, Martin Suda, Andrei Voronkov and Krystof Hoder. Selecting the Selection
14:30--15:00
 Stephan Schulz and Martin Mohrmann. Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
15:00--15:20  [SD]
 Gabriel Ebner, Stefan Hetzl, Giselle Reis, Martin Riener, Simon Wolfsteiner and Sebastian Zivota. System Description: GAPT 2.0
15:20--15:40  [SD]
 Jens Otten. NanoCoP: A Non-clausal Connection Prover

15:40--16:10  Break

16:10--17:30  Session Verification I

16:10--16:40  
 Taolue Chen, Xincai Gu and Zhilin Wu. A complete decision procedure for linearly compositional separation logic with data constraints
16:40--17:10
 Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt and Juergen Giesl. Lower Runtime Bounds for Integer Programs
17:10--17:30  [SD]
 Francisco Duran, Steven Eker, Santiago Escobar, Narciso Marti-Oliet, Jose Meseguer and Carolyn Talcott. Built-in Variant Generation and Unification, and their Applications in Maude 2.7 

17:30--17:45  Break

17:45--18:45  Awards (Herbrand Award and Best Paper Award)
19:00--       Welcome reception

  
TUESDAY June 28:

09:00--10:00  Invited Talk 
 Gilles Barthe.  Verification of differential private computations
10:00--10:30  
 Joseph Boudou. Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition

10:30--11:00  Break

11:00--12:30  Session  Non-classical Logics

11:00--11:30
 Diana Costa and Manuel A. Martins. A Tableau System for Quasi-Hybrid Logic
11:30--12:00
 Simon Docherty and David Pym. Intuitionistic layered graph logic
12:00--12:30
 Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron and Pietro Sala. Interval Temporal Logic Model Checking: the Border Between Good and Bad HS Fragments

12:30--14:00  Lunch

14:00--15:40  Session  Modal Logics

14:00--14:30
 Jeremy Dawson, James Brotherston and Rajeev Gore. Machine-checked Interpolation Theorems for Substructural Logics using Display Calculi
14:30--15:00
 Revantha Ramanayake. Inducing syntactic cut-elimination for indexed nested sequents
15:00--15:20  [SD]
 Yoni Zohar and Anna Zamansky. Gen2sat: an Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi
15:20--15:40  [SD]
 Claudia Nalon, Ullrich Hustadt and Clare Dixon. KSP: A resolution-based prover for multimodal K

15:40--16:10  Break

16:10--17:30  Session Proof Theory, Interpolation, and Rewriting

16:10--16:40
 David Cerna and Alexander Leitsch. Schematic Cut elimination and the Ordered Pigeonhole Principle
16:40--17:10
 Viorica Sofronie-Stokkermans. On Interpolation and Symbol Elimination in Theory Extensions
17:10--17:30 [SD]
 Takahito Aoto and Kentaro Kikuchi. Nominal Confluence Tool

WEDNESDAY June 29

09:00--10:00  Invited Talk 
 Arnon Avron.  A logical framework for developing and mechanizing set theories
10:00--10:30  
 Takuya Matsuzaki, Hidenao Iwane, Munehiro Kobayashi, Yiyang Zhan, Ryoya Fukasaku, Jumma Kudo, Hirokazu Anai and Noriko Arai. Race against the Teens -- Benchmarking Mechanized Math on Pre-university Problems

10:30--11:00  Break

11:00--12:30  Session Verification II

11:00--11:30
 Francesco Alberti, Silvio Ghilardi and Elena Pagani. Counting Constraints in Flat Array Fragments
11:30--12:00
 Benjamin Aminof and Sasha Rubin. Model Checking Parameterised Multi-Token Systems via the Composition Method
12:00--12:30
 Konstantinos Athanasiou, Peizun Liu and Thomas Wahl. Unbounded-Thread Program Verification using Thread-State Equations

12:30--14:00  Lunch

14:00--15:45  Business Meetings

16:00--       Social Program


THURSDAY June 30

09:00--10:00  Invited Talk 
 Andre Platzer.  Logic and proofs for cyber-physical systems
10:00--10:30  
 Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur and Mingshuai Chen. Interpolation synthesis for quadratic polynomial inequalities and combination with EUF

10:30--11:00  Break

11:00--12:30  Session Satisfiability-Module Theories

11:00--11:30
 Leonardo de Moura and Daniel Selsam. Congruence Closure in Intensional Type Theory
11:30--12:00 
 Roberto Sebastiani. Colors Make Theories Hard
12:00--12:30
 Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes and Cesare Tinelli. Model Finding for Recursive Functions in SMT

12:30--14:00  Lunch

14:00--15:50  Session  Satisfiability Modulo Theories 

14:00--14:30
 Martin Bromberger and Christoph Weidenbach. Fast Cube Tests for LIA Constraint Solving
14:30--15:00
 Kshitij Bansal, Clark Barrett, Andrew Reynolds and Cesare Tinelli.  A new decision procedure for finite sets and cardinality in SMT
15:00--15:20 [SD]
 Vu Xuan Tung, To Van Khanh and Mizuhito Ogawa. raSAT : SMT Solver for Polynomial Constraints
15:20--15:50
 Hans De Nivelle. Subsumption Algorithms for Three-Valued Geometric Resolution

15:40--16:10  Break

16:10--17:20  Session Higher-order logic

16:10--16:40 
 Michael Farber and Chad Brown. Internal guidance for Satallax
16:40--17:00 [SD]
 Max Wisniewski, Alexander Steen, Kim Kern and Christoph Benzmueller. Effective Normalization Techniques for HOL
17:00--17:20 [SD]
 Lars Hupel and Viktor Kuncak. Translating Scala Programs to Isabelle/HOL