21. CADE 2007: Bremen, Germany

Session 1. Invited Talk: Colin Stirling

• Colin Stirling:
  Games, Automata and Matching. 1-2
  

Session 2. Higher-Order Logic

• Osman Hasan, Sofiène Tahar:
  Formalization of Continuous Probability Distributions. 3-18
  
• Guodong Li, Konrad Slind:
  Compilation as Rewriting in Higher Order Logic. 19-34
  
• Christian Urban, Stefan Berghofer, Michael Norrish:
  Barendregt's Variable Convention in Rule Inductions. 35-50
  
• John Harrison:
  Automating Elementary Number-Theoretic Proofs Using Gröbner Bases. 51-66
  

Session 3. Description Logic

• Boris Motik, Rob Shearer, Ian Horrocks:
  Optimized Reasoning in Description Logics Using Hypertableaux. 67-83
  
• Carsten Lutz, Frank Wolter:
  Conservative Extensions in the Lightweight Description Logic EL. 84-99
  
• Gulay Ünel, David Toman:
  An Incremental Technique for Automata-Based Decision Procedures. 100-115
  

Session 4. Intuitionistic Logic

• Samuli Heilala, Brigitte Pientka:
  Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. 116-131
  
• Roger Antonsen, Arild Waaler:
  A Labelled System for IPL with Variable Splitting. 132-146
  

Session 5. Invited Talk: Ashish Tiwari

• Ashish Tiwari, Sumit Gulwani:
  Logical Interpretation: Static Program Analysis Using Theorem Proving. 147-166
  

Session 6. Satisfiability Modulo Theories

• Yeting Ge, Clark Barrett, Cesare Tinelli:
  Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. 167-182
  
• Leonardo Mendonça de Moura, Nikolaj Bjørner:
  Efficient E-Matching for SMT Solvers. 183-198
  
• Maria Paola Bonacina, Mnacho Echenim:
  T-Decision by Decomposition. 199-214
  
• Viktor Kuncak, Martin C. Rinard:
  Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. 215-230
  

Session 7. Induction, Rewriting, and Polymorphism

• Markus Aderhold:
  Improvements in Formula Generalization. 231-246
  
• Guillem Godoy, Sophie Tison:
  On the Normalization and Unique Normalization Properties of Term Rewrite Systems. 247-262
  
• Jean-François Couchot, Stéphane Lescuyer:
  Handling Polymorphism in Automated Deduction. 263-278
  

Session 8. First-Order Logic

• Peter Höfner, Georg Struth:
  Automated Reasoning in Kleene Algebra. 279-294
  
• Geoff Sutcliffe, Yury Puzis:
  SRASS - A Semantic Relevance Axiom Selection System. 295-310
  
• Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv:
  Labelled Clauses. 311-327
  
• Christopher Lynch, Duc-Khanh Tran:
  Automatic Decidability and Combinability Revisited. 328-344
  

Session 9. Invited Talk: K. Rustan M. Leino

• K. Rustan M. Leino:
  Designing Verification Conditions for Software. 345
  

Session 10. Model Checking and Verification

• Juan Antonio Navarro Pérez, Andrei Voronkov:
  Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. 346-361
  
• Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli:
  Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. 362-378
  
• Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt:
  The KeY system 1.0 (Deduction Component). 379-384
  
• Oleg Mürk, Daniel Larsson, Reiner Hähnle:
  KeY-C: A Tool for Verification of C Programs. 385-390
  
• David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu:
  The Bedwyr System for Model Checking over Syntactic Expressions. 391-397
  
• Konstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich:
  System for Automated Deduction (SAD): A Tool for Proof Verification. 398-403
  

Session 11. Invited Talk: Peter Baumgartner

• Peter Baumgartner:
  Logical Engineering with Instance-Based Methods. 404-409
  

Session 12. Termination

• Adam Koprowski, Aart Middeldorp:
  Predictive Labeling with Dependency Pairs Using SAT. 410-425
  
• Stephan Falke, Deepak Kapur:
  Dependency Pairs for Rewriting with Non-free Constructors. 426-442
  
• Jürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp:
  Proving Termination by Bounded Increase. 443-459
  
• Alexander Krauss:
  Certified Size-Change Termination. 460-475
  

Session 13. Tableaux and First-Order Systems

• Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor:
  Encoding First Order Proofs in SAT. 476-491
  
• Peter Baumgartner, Ulrich Furbach, Björn Pelzer:
  Hyper Tableaux with Equality. 492-507
  
• Björn Pelzer, Christoph Wernhard:
  System Description: E-KRHyper. 508-513
  
• Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic:
  System Description: SpassVersion 3.0. 514-520
  

Last update Sun May 19 21:46:33 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page