Programme
The technical programme is converging to a final version: we also have a list of accepted papers and satellite events as well as guest speakers and invited speakers.
Monday, June 25th: registration opens at 16:00, closes around 19:00.
Tuesday, June 26th:
- 9:00 – 10:00: invited talk by Yuri Matiyasevich (chair: Bernhard Gramlich):
Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics - 10:00 – 10:30: Morning Coffee Break
- 10:30 – 12:00: Arithmetic: SAT-Solving, Decision Procedures and Induction,
chair: Peter Baumgartner- François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout and Guillaume Melquiond: A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
- Stephan Falke and Deepak Kapur: Rewriting Induction + Linear Arithmetic = Decision Procedure
- Dejan Jovanović and Leonardo De Moura: Solving Non-Linear Arithmetic
- 12:00 – 13:15: Lunch Break
- 13:15 – 14:45: Temporal Logic, chair: Florent Jacquemard
- Pierre-Cyrille Heam, Vincent Hugot and Olga Kouchnarenko:
From Linear Temporal Logic Properties to Rewrite Propositions - Markus Latte and Martin Lange:
Branching Time? Pruning Time! - Stéphane Demri, Amit Kumar Dhar and Arnaud Sangnier:
Taming Past LTL and Flat Counter Systems
- Pierre-Cyrille Heam, Vincent Hugot and Olga Kouchnarenko:
- 14:45 – 15:15: Afternoon Coffee Break
- 15:15 – 16:45: Non-Classical Logics, chair: Hans de Nivelle
- Jan-David Quesel and Andre Platzer:
Playing Hybrid Games with KeYmaera - Matthias Baaz, Ori Lahav and Anna Zamansky:
Effective Finite-valued Semantics for Labelled Calculi - Rajeev Gore and Jimmy Thomson:
BDD-based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics
- Jan-David Quesel and Andre Platzer:
- 18:00 – 18:30: Afternoon Coffee Break in Whitworth Hall (Building 50 on this map)
- 18:30 – 19:30: Herbrand Award Ceremony in Whitworth Hall
- from 19:30: Reception in Christie’s Bistro (Building 58 on this map)
Wednesday, June 27th:
- 9:00 – 10:00: invited talk by Robert Nieuwenhuis (chair: Uli Sattler):
SAT and SMT Are Still Resolution: Questions and Challenges - 10:00 – 10:30: Morning Coffee Break
- 10:30 – 12:00: SMT-Solving and Real Arithmetic, chair: Reiner Hähnle
- Sicun Gao, Jeremy Avigad and Edmund Clarke:
Delta-Complete Decision Procedures for Satisfiability over the Reals - Andrej Spielmann and Viktor Kuncak:
Synthesis for Unbounded Bitvector Arithmetic - Roberto Sebastiani and Silvia Tomasi:
Optimization in SMT with LA(Q) Cost Functions
- Sicun Gao, Jeremy Avigad and Edmund Clarke:
- 12:00 – 13:30: Lunch Break
- 13:30 – 15:00: Unification, chair: Silvio Ghilardi
- Andrew Marshall and Paliath Narendran:
A New Algorithm for Unification Modulo One-Sided Distributivity - Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran and Michael Rusinowitch: Unification modulo Synchronous Distributivity
- Franz Baader, Stefan Borgwardt and Barbara Morawska:
SAT-Encoding of Unification in ELHR+ w.r.t. Cycle-Restricted Ontologies
- Andrew Marshall and Paliath Narendran:
- 15:00 – 15:30: Afternoon Coffee Break
- 15:30 – 17:00: Fixed Points and Combination Issues, chair: Jürgen Giesl
- Alwen Tiu: Stratification in Logics of Definitions
- Roberto Bruttomesso, Silvio Ghilardi and Silvio Ranise: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
- Pascal Fontaine, Stephan Merz and Christoph Weidenbach:
Combination of disjoint theories: beyond decidability
- 17:30 – 18:30: Afternoon Lecture by Peter Andrews (chair: Andrei Voronkov)
- 18:30 – 19:30: CADE and IJCAR Business Meetings
- from 19:45: Competition Dinner
Thursday, June 28th:
- 9:00 – 10:00: invited talk by Nicole Schweikardt (chair: Birte Glimm):
Querying graph structured data - 10:00 – 10:30: Morning Coffee Break and Start of CASC-J6
- 10:30 – 12:00: Description Logics, chair: Franz Baader
- Stefan Borgwardt, Felix Distel and Rafael Peñaloza:
How Fuzzy is my Fuzzy Description Logic? - Andreas Steigmiller, Thorsten Liebig and Birte Glimm:
Extended Caching, Backjumping and Merging for Expressive Description Logics - Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Geneves and Nabil Layaïda:
SPARQL Query Containment under RDFS Entailment Regime
- Stefan Borgwardt, Felix Distel and Rafael Peñaloza:
- 12:00 – 13:30: Lunch Break with
- 12:30-13:00: TABLEAUX Business Meeting
- 13:30 – 15:00: Higher-Order and Non-Classical Logics, chair: Alwen Tiu
- Frank de Boer, Marcello Bonsangue and Jurriaan Rot: Automated Verification of Recursive Programs with Pointers
- Taus Brock-Nannestad and Carsten Schuermann:
Truthful Monadic Abstractions - Chad Brown: Satallax: An Automated Higher-Order Prover (system description)
- Thomas Raths and Jens Otten: The QMLTP Problem Library for First-order Modal Logics (system description)
- 15:00 – 15:30: Afternoon Coffee Break
- 15:30 – 17:00: Systems Related Full Papers, chair: Christoph Weidenbach
- Matti Järvisalo, Marijn Heule and Armin Biere: Inprocessing Rules
- Daniel Kuehlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban and Tom Heskes: Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel and Andrei Voronkov: EPR-based bounded model checking at word level
- 17:30 – 18:30: Afternoon Lecture by Martin Davis (chair: Konstantin Korovin)
- from 19:45: Ceilidh with Albireo in Jabez Clegg
Friday, June 29th:
- 9:00 – 10:00: invited talk by Nikolaj Bjorner (chair: Geoff Sutcliffe):
Taking Satisfiability to the Next Level with Z3 - 10:00 – 10:30: Morning Coffee Break
- 10:30 – 12:00: Applications I: Termination and Reachability Analysis, chair: Viorica Sofronie-Stokkermans
- Đurica Nikolić and Fausto Spoto:
Reachability Analysis of Program Variables - Conrad Rau, David Sabel and Manfred Schmidt-Schauss:
Correctness of Program Transformations as a Termination Problem - Fabian Emmes, Tim Enger and Jürgen Giesl:
Proving Non-Looping Non-Termination Automatically
- Đurica Nikolić and Fausto Spoto:
- 12:00 – 13:15: Lunch Break
- 13:15 – 15:00: System Descriptions & Termination Competition, chair: Christopher Lynch
- Jürgen Giesl: Results from Termination Competition
- Mélanie Jacquel, Karim Berkani, David Delahaye and Catherine Dubois:
Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover - Thomas Sternagel and Harald Zankl:
KBCV – Knuth-Bendix Completion Visualizer - Stephan Schulz:
Fingerprint Indexing for Paramodulation and Rewriting - Boris Konev, Michel Ludwig and Frank Wolter:
Logical Difference Computation with CEX 2.5 - Matej Urbas and Mateja Jamnik:
Diabelli: A heterogeneous reasoning framework - Martin Suda and Christoph Weidenbach:
A PLTL-prover based on labelled superposition with partial model guidance - Franz Baader, Julian Mendez and Barbara Morawska:
UEL: Unification Solver for the Description Logic EL, System Description
- 15:00 – 15:30: Afternoon Coffee Break
- 15:30 – 17:00: Applications II: Mathematical Structures, Explanation Generation, Security, chair: Maria Paola Bonacina
- Simon Foster and Georg Struth: Automated Analysis of Regular Algebra
- Mnacho Echenim and Nicolas Peltier:
A Calculus for Generating Ground Explanations - Stephanie Delaune, Steve Kremer and Daniel Pasaila:
Security protocols, constraint systems, and group theories
- 17:30 – 18:45: Afternoon Lecture by John Alan Robinson (chair: Andrei Voronkov)
followed by Geoff Sutcliffe: CASC data description - from 19:45: Conference Dinner
Saturday, June 30th and Sunday,. July 1st: Satellite Events