22. CADE 2009: Montreal, Canada

Invited Talk

• Martin C. Rinard:
  Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival. 1-16
  

Combinations and Extensions

• Peter Baumgartner, Uwe Waldmann:
  Superposition and Model Evolution Combined. 17-34
  
• Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura:
  On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving. 35-50
  
• Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch:
  Combinable Extensions of Abelian Groups. 51-66
  
• Viorica Sofronie-Stokkermans:
  Locality Results for Certain Extensions of Theories with Bridging Functions. 67-83
  

Minimal Unsatisfiability and Automated Reasoning Support

• Roberto Sebastiani, Michele Vescovi:
  Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. 84-99
  
• Éric Grégoire, Bertrand Mazure, Cédric Piette:
  Does This Set of Clauses Overlap with at Least One MUS? 100-115
  
• Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss:
  Progress in the Development of Automated Theorem Proving for Higher-Order Logic. 116-130
  

System Descriptions

• Carsten Ihlemann, Viorica Sofronie-Stokkermans:
  System Description: H-PILoT. 131-139
  
• Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski:
  SPASS Version 3.5. 140-145
  
• Hicham Bensaid, Ricardo Caferra, Nicolas Peltier:
  Dei: A Theorem Prover for Terms with Integer Exponents. 146-150
  
• Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine:
  veriT: An Open, Trustable and Efficient SMT-Solver. 151-156
  
• Alex Roederer, Yury Puzis, Geoff Sutcliffe:
  Divvy: An ATP Meta-system Based on Axiom Relevance Ordering. 157-162
  

Invited Talk

• Konstantin Korovin:
  Instantiation-Based Automated Reasoning: From Theory to Practice. 163-166
  

Interpolation and Predicate Abstraction

• Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
  Interpolant Generation for UTVPI. 167-182
  
• Amit Goel, Sava Krstic, Cesare Tinelli:
  Ground Interpolation for Combined Theories. 183-198
  
• Laura Kovács, Andrei Voronkov:
  Interpolation and Symbol Elimination. 199-213
  
• Shuvendu K. Lahiri, Shaz Qadeer:
  Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. 214-229
  

Resolution-Based Systems for Non-classical Logics

• Sean McLaughlin, Frank Pfenning:
  Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. 230-244
  
• Lan Zhang, Ullrich Hustadt, Clare Dixon:
  A Refined Resolution Calculus for CTL. 245-260
  
• Michel Ludwig, Ullrich Hustadt:
  Fair Derivations in Monodic Temporal Reasoning. 261-276
  

Termination Analysis and Constraint Solving

• Stephan Falke, Deepak Kapur:
  A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. 277-293
  
• Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodríguez-Carbonell, Albert Rubio:
  Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. 294-305
  

Invited Talk

• Mark E. Stickel:
  Building Theorem Provers. 306-321
  

Rewriting, Termination and Productivity

• Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, Peter Schneider-Kamp:
  Termination Analysis by Dependency Pairs and Inductive Theorem Proving. 322-338
  
• Martin Korp, Aart Middeldorp:
  Beyond Dependency Graphs. 339-354
  
• Stefan Ciobâca, Stéphanie Delaune, Steve Kremer:
  Computing Knowledge in Security Protocols under Convergent Equational Theories. 355-370
  
• Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks:
  Complexity of Fractran and Productivity. 371-387
  

Models

• Koen Claessen, Ann Lillieström:
  Automated Inference of Finite Unsatisfiability. 388-403
  
• Matthias Horbach, Christoph Weidenbach:
  Decidability Results for Saturation-Based Model Building. 404-420
  

Modal Tableaux with Global Caching

• Linh Anh Nguyen, Andrzej Szalas:
  A Tableau Calculus for Regular Grammar Logics with Converse. 421-436
  
• Rajeev Goré, Florian Widmann:
  An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability. 437-452
  

Arithmetic

• Feifei Ma, Sheng Liu, Jian Zhang:
  Volume Computation for Boolean Combination of Linear Arithmetic Constraints. 453-468
  
• Bernard Boigelot, Julien Brusten, Jérôme Leroux:
  A Generalization of Semenov's Theorem to Automata over Real Numbers. 469-484
  
• André Platzer, Jan-David Quesel, Philipp Rümmer:
  Real World Verification. 485-501