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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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

  • Calendar of Events

    ⇐ ⇒June 2014
    SMTWTFS
    1234567
    891011121314
    15161718192021
    22232425262728
    293012345