Montreal architectural style

CADE-22

22nd International Conference on Automated Deduction
McGill University, Montreal, Canada
August 2 - 7, 2009

CADE-22 Conference Schedule

For your convenience, we also provide the conference schedule in PDF format.

Monday, August 3

 18:30-20:30 Welcome Reception at McCord Museum

Tuesday, August 4

 08:55-9:00 Welcome
   Brigitte Pientka (Conference Chair)
 09:00-10:00 Session 1: Invited Talk Chair: Aaron Stump
  Integrated Reasoning and Proof Choice Point Selection in the Jahob System: Mechanisms for Program Survival
   Martin Rinard
  10:00-10:30 Coffee Break
 10:30-12:30 Session 2: Combinations and Extensions Chair: Nikolaj Bjørner
 10:30 Superposition and Model Evolution Combined
   Peter Baumgartner and Uwe Waldmann
  11:00 On Deciding Satisfiability by DPLL( $\Gamma+{\cal T}$) and Unsound Theorem Proving
   Maria Paola Bonacina, Christopher Lynch and Leonardo de Moura
  11:30 Combinable Extensions of Abelian Groups
   Enrica Nicolini, Christophe Ringeissen and Michaël Rusinowitch
  12:00 Locality Results for Certain Extensions of Theories with Bridging Functions
   Viorica Sofronie-Stokkermans
  12:30-14:00 Catered Lunch
 14:00-15:30 Session 3: Minimal Unsatisfiability and Automated Reasoning Support Chair: Carsten Schürmann
 14:00 Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis
   Roberto Sebastiani and Michele Vescovi
  14:30 Does this Set of Clauses Overlap with at least one MUS?
   Éric Grégoire, Bertrand Mazure and Cédric Piette
  15:00 Progress in the Development of Automated Theorem Proving for Higher-Order Logic
   Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown and Frank Theiss
  15:30-16:00 Coffee Break
 16:00-17:40 Session 4: System Descriptions Chair: Peter Baumgartner
 16:00 System Description: H-PILoT
   Carsten Ihlemann and Viorica Sofronie-Stokkermans
  16:20 SPASS Version 3:5
   Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda and Patrick Wischnewski
  16:40 DEI: A Theorem Prover for Terms with Integer Exponents
   Hicham Bensaid, Ricardo Caferra and Nicolas Peltier
  17:00 veriT: An Open, Trustable and Efficient SMT-Solver
   Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe and Pascal Fontaine
  17:20 Divvy: An ATP Meta-system Based on Axiom Relevance Ordering
   Alex Roederer, Yury Puzis and Geoff Sutcliffe
  17:40-17:50 Handover of Festschrift to Peter B. Andrews
   Christoph Benzmüller (Co-Editor)
 17:50-19:00 CADE Business Meeting
   Reiner Hähnle (Vice-President)

Wednesday, August 5

 09:00-10:00 Session 5: Invited Talk Chair: Cesare Tinelli
  Instantiation-Based Automated Reasoning: From Theory to Practice
   Konstantin Korovin
  10:00-10:30 Coffee Break
 10:30-12:30 Session 6: Interpolation and Predicate Abstraction
   Chair: Maria Paola Bonacina
 10:30 Interpolant Generation for UTVPI
   Alessandro Cimatti, Alberto Griggio and Roberto Sebastiani
  11:00 Ground Interpolation for Combined Theories
   Amit Goel, Sava Krstic and Cesare Tinelli
  11:30 Interpolation and Symbol Elimination
   Laura Kovács and Andrei Voronkov
  12:00 Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
   Shuvendu K. Lahiri and Shaz Qadeer
  12:30-14:00 Catered Lunch
 14:00-15:30 Session 7: Resolution-Based Systems for Non-classical Logics Chair: Hans de Nivelle
 14:00 Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
   Sean McLaughlin and Frank Pfenning
  14:30 A Refined Resolution Calculus for CTL
   Lan Zhang, Ullrich Hustadt and Clare Dixon
  15:00 Fair Derivations in Monodic Temporal Reasoning
   Michel Ludwig and Ullrich Hustadt
  15:30-16:00 Coffee Break
 16:00-17:00 Session 8: Termination Analysis and Constraint Solving
   Chair: Christopher Lynch
 16:00 A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
   Stephan Falke and Deepak Kapur
  16:30 Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
   Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodríguez-Carbonell and Albert Rubio
  17:00-18:00 Presentation of the Herbrand Award to Deepak Kapur
   Reiner Hähnle (Master of Ceremony)

Thursday, August 6

 09:00-10:00 Session 9: Invited Talk Chair: Geoff Sutcliffe
  Building Theorem Provers
   Mark E. Stickel
  10:00-10:30 Coffee Break
 10:30-12:30 Session 10: Rewriting, Termination and Productivity
   Chair: Christoph Weidenbach
 10:30 Termination Analysis by Dependency Pairs and Inductive Theorem Proving
   Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs and Peter Schneider-Kamp
  11:00 Beyond Dependency Graphs
   Martin Korp and Aart Middeldorp
  11:30 Computing Knowledge in Security Protocols under Convergent Equational Theories
   Stefan Ciobâca, Stéphanie Delaune and Steve Kremer
  12:00 Complexity of Fractran and Productivity
   Jörg Endrullis, Clemens Grabmayer and Dimitri Hendriks
  12:30-14:00 Catered Lunch
 14:00- Excursion and Banquet at Pointe-à-Callière

Friday, August 7

 09:00-10:00 Session 11: Models Chair: Albert Oliveras
 09:00 Automated Inference of Finite Unsatisfiability
   Koen Claessen and Ann Lillieström
  09:30 Decidability Results for Saturation-Based Model Building
   Matthias Horbach and Christoph Weidenbach
  10:00-10:30 Coffee Break
 10:30-11:30 Session 12: Modal Tableaux with Global Caching
   Chair: Ullrich Hustadt
 10:30 A Tableau Calculus for Regular Grammar Logics with Converse
   Linh Anh Nguyen and Andrzej Szałas
  11:00 An Optimal On-the-fly Tableau-Based Decision Procedure for PDL-Satisfiability
   Rajeev Goré and Florian Widmann
  11:30-12:30 System Competition Results Chair: Renate Schmidt
 11:30 CASC: The CADE ATP System Competition
   Geoff Sutcliffe
 12:00 SMT-COMP: Satisfiability Modulo Theories Competition
   Albert Oliveras
 12:30-14:00 Catered Lunch
 14:00-15:30 Session 13: Arithmetic Chair: Reiner Hähnle
 14:00 Volume Computation for Boolean Combination of Linear Arithmetic Constraints
   Feifei Ma, Sheng Liu and Jian Zhang
  14:30 A Generalization of Semenov's Theorem to Automata over Real Numbers
   Bernard Boigelot, Julien Brusten and Jérôme Leroux
  15:00 Real World Verification
   André Platzer, Jan-David Quesel and Philipp Rümmer
  15:30-16:00 Coffee Break