[TYPES] CADE'05: Call for Participation and Accepted Papers

[Brigitte Pientka]

----------------------------------------------------------
                         CADE-20
       20th International Conference on Automated Deduction
            Tallinn, Estonia, July 22 - July 27, 2005
                http://deepthought.ttu.ee/it/cade/

                   CALL FOR PARTICIPATION

-----------------------------------------------------------
    IMPORTANT DATES:

   Deadline for early registration: 20. June, 2005.
   Deadline for non-cash payments: 12. July, 2005.
   Workshops: July 22-23, 2005
   Conference: July 24-27, 2005
-----------------------------------------------------------

CADE is the major forum for the presentation of research
in all aspects of automated deduction.

     INVITED TALKS:

Invited talks will be given at CADE-20 by Randal Bryant (CMU), Gilles
Dowek (Ecole Polytechnique) and by Frank Wolter (U. Liverpool).

     INVITED TUTORIALS:

- Bruno Blanchet
  An Automatic Security Protocol Verifier based on
  Resolution Theorem Proving

- Enrico Giunchiglia
  Beyond SAT: QSAT, and SAT-based Decision Procedures


      ACCEPTED PAPERS:

- Tomasz Truderung:
  Regular Protocols and Attacks with Regular Knowledge

- Greta Yorsh and Madan Musuvathi:
  A Combination Method for Generating Interpolants

- Ullrich Hustadt, Boris Konev and Renate A. Schmidt.
  Deciding monodic fragments by temporal resolution

- Guillaume Dufay, Amy Felty and Stan Matwin.
  Privacy-Sensitive Information Flow with JML

- Viktor Kuncak, Hai, Huu Nguyen and Martin Rinard.
  An Algorithm for Deciding BAPA: Boolean Algebra with Presburger
  Arithmetic

- Franz Baader and Silvio Ghilardi.
  Connecting many-sorted theories

- Claudio Castellini and Alan Smaill.
  Proof Planning for First-Order Temporal Logic

- Graham Steel.
  Deduction with XOR Constraints in Security API Modelling

- Tal Lev-Ami, Neil Immerman, Siddharth Srivastava, Greta Yorsh, Mooly
  Sagiv and Thomas W. Reps.
  Simulating Reachability using First-Order Logic with Applications to
  Verification of Linked Data Structures

- Viorica Sofronie-Stokkermans.
  Hierarchic reasoning in local theory extensions

- Kaustuv Chaudhuri and Frank Pfenning.
  A Focusing Inverse Method Prover for First-Order Linear Logic

- Mizuhito Ogawa, Eiichi Horita and Satoshi Ono.
  Proving Properties of Incremental Merkel Trees

- Evelyne Contejean and Pierre Corbineau.
  Reflecting Proofs in First-Order Logic with Equality

- Chad Brown.
  Reasoning in Extensional Type Theory with Equality

- Christian Fermueller and Reinhard Pichler.
  Model Representation via Contexts and Implicit Generalizations

- Peter Baumgartner and Cesare Tinelli.
  ME-E -- The Model Evolution Calculus with Equality

- Brigitte Pientka.
  Tabling for higher-order logic programming

- Christian Urban and Christine Tasson.
  Nominal Techniques in Isabelle/HOL

- Kumar Neeraj Verma, Helmut Seidl and Thomas Schwentick.
  On the Complexity of Equational Horn Clauses

- Jordi Levy, Mateu Villaret and Joachim Niehren.
  Well-Nested Context Unification

- Serge R. Autexier.
  The CORE Calculus

- Guillem Godoy and Ashish Tiwari.
  Termination of Rewrite Systems with Shallow Right-Linear,
  Collapsing, and Right-Ground Rules

- Jian Zhang.
  Computer Search for Counterexamples to Wilkie's Identity

- John Harrison and Sean McLaughlin.
  A Proof Producing Decision Procedure for Real Arithmetic

- Ting Zhang, Henny Sipma and Zohar Manna.
  The Decidability of the First-order theory of Knuth-Bendix Order


     SYSTEM DESCRIPTIONS

- Sean Bechhofer, Ian Horrocks and Daniele Turi.
  The OWL Instance Store (System Description)

- Andreas Meier and Erica Melis.
  MULTI: A Multi-Strategy Proof Planner (System Description)

- Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi
  Junttila, Peter van Rossum, Stephan Schulz and Roberto Sebastiani.
  MathSAT 3 (System Description)

- Marco Benedetti.
  sKizzo: A Suite to Evaluate and Certify QBFs (System Description)

- Alex Sinner and Thomas Kleemann.
  KRHyper - In Your Pocket (System Description)


     WORKSHOPS AND TUTORIALS:

- Empirically Successful Classical Automated Reasoning (ESCAR)
  Geoff Sutcliffe, Stephan Schulz, and Bernd Fischer

- Workshop on Disproving: Non-Theorems, Non-Validity, Non-Provability
  Wolfgang Ahrendt, Peter Baumgartner and Hans de Nivelle

-  Empirically Successful Classical Automated Reasoning (ESCAR)
   Geoff Sutcliffe, Stephan Schulz, and Bernd Fischer

- Constraints in Formal Verification 2005 (CFV'05).
  Joao Marques-Silva, Miroslav Velev

- Tutorial: Integrating Object-Oriented Design and
             Deductive Verification of Software
  Wolfgang Ahrendt, Bernhard Beckert, Reiner Haehnle, Peter Schmitt

---------------------------------------------------------------------

   Organizing Chair:                 Tanel Tammet (Tallinn TU)
   Workshop and Tutorial Chair:      Frank Pfenning (CMU)
   Program Chair:                    Robert Nieuwenhuis (UPC Barcelona)
   Publicity Chair:                  Brigitte Pientka (McGill)

--------------------------------------------------------------------