Automated Deduction: Decidability, Complexity, Tractability
(ADDCT'07)

Affiliated with CADE-21 Bremen, Germany, 15 July, 2007

All sessions will take place at the International University Bremen, in the West Hall. Click here for a map of the campus.

Invited speaker

Michaël Rusinowitch (LORIA-INRIA-Lorraine)

Program

Abstracts

ADDCT proceedings

Registration

Organizers

  • Silvio Ghilardi (U. Milano)
  • Ulrike Sattler (U. Manchester)
  • Viorica Sofronie-Stokkermans (MPI,Saarbrücken)
  • Ashish Tiwari (Menlo Park)

    • Program Committee

  • Matthias Baaz (T.U.Wien)
  • Maria Paola Bonacina (U. Verona)
  • Christian Fermüller (T.U.Wien)
  • Silvio Ghilardi (U. Milano)
  • Reiner Haehnle (Chalmers U.)
  • Felix Klaedtke (ETH Zurich)
  • Sava Krstic (Intel Corporation)
  • Viktor Kuncak (EPFL Lausanne)
  • Carsten Lutz (TU Dresden)
  • Christopher Lynch (Clarkson U.)
  • Silvio Ranise (LORIA/INRIA-Lorraine)
  • Ulrike Sattler (U. Manchester)
  • Renate Schmidt (U. Manchester)
  • Viorica Sofronie-Stokkermans (MPI,Saarbrücken)
  • Ashish Tiwari (SRI)
  • Luca Vigano (U. Verona)

    • Call for papers

    Topics

    Submission procedure

    Publication

    Important Dates

  • 11 May 2007: Submission deadline
  • 5 June 2007: Notification
  • 15 June 2007: Final version
  • 15 July 2007: Workshop

    • Contact

    For further informations please send an e-mail to sofronie@mpi-inf.mpg.de

    Tentative Program (Sunday, July 15th)

    09:30-10:30 Session 1: Invited talk

    09:30-10:30   Michaël Rusinowitch (LORIA-INRIA-Lorraine)
    Some Decision Problems Related to Cryptographic Protocol Verification

    10:30-11:00 Coffee Break

    11:00-12:30 Session 2: Decidable fragments of first-order logic and applications

    11:00-11:35   Stephanie Delaune, Hai Lin and Christopher Lynch
    Protocol Verification via Rigid/Fleixble Resolution
    11:35-12:10   Aharon Abadi, Alexander Rabinovich and Mooly Sagiv
    Decidable Fragments of Many Sorted Logic
    12:10-12:30   Maria Paola Bonacina and Mnacho Echenim
    Decision procedures for variable-inactive theories and two polynomial T-satisfiability procedures

    12:30-14:00 Lunch Break

    14:00-15:30 Session 3: Decidability in intuitionistic, modal and description logics

    14:00-14:35   Linh Anh Nguyen
    Approximating Horn Knowledge Bases in Regular Description Logics to Have PTIME Data Complexity
    14:35-15:10   Didier Galmiche and Daniel Mery
    Connection-based proof search in intuitionistic logic from transitive closure of constraints
    15:10-15:30   Carsten Lutz and Frank Wolter
    Conservative extensions in modal and description logics

    15:30-16:00 Coffee Break

    16:00-17:00 Session 4: Combinations of decision procedures

    16:00-16:20   Sava Krstic, Amit Goel, Jim Grundy and Cesare Tinelli.
    Combined Satisfiability Modulo Parametric Theories
    16:20-16:40   Leonardo de Moura, and Nikolaj Bjorner
    Model-based Theory Combination
    16:40-17:00   Viktor Kuncak, Charles Bouillaguet, Thomas Wies, Karen Zee and Martin Rinard.
    Decision procedures for data structure verification