[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] CADE-22 last call for papers




LAST CALL FOR PAPERS


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


Submission Deadline: 23 Feb 2009 http://complogic.cs.mcgill.ca/cade22/


GENERAL INFORMATION CADE is the major forum for the presentation of research in all aspects of automated deduction. The conference programme will include invited talks, paper presentations, system descriptions, workshops, tutorials, and system competitions.

SCOPE
We invite high-quality submissions on the general topic of
automated deduction, including foundations, applications,
implementations and practical experiences.


Logics of interest include, but are not limited to

   o propositional, first-order, equational, higher-order,
     classical, description, modal, temporal, many-valued,
     intuitionistic, other non-classical, meta-logics,
     logical frameworks, type theory and set theory.

Methods of interest include, but are not limited to

   o saturation, resolution, instance-based, tableaux, sequent
     calculi, natural deduction, term rewriting, decision
     procedures, model generation, model checking, constraint
     solving, induction, unification, proof planning, proof
     checking, proof presentation and explanation.

Applications of interest include, but are not limited to

   o program analysis and verification, hardware verification,
     mathematics, natural language processing, computational
     linguistics, knowledge representation, ontology reasoning,
     deductive databases, functional and logic programming,
     robotics, planning, and other areas of AI.

INVITED SPEAKERS:
 Konstantin Korovin   The University of Manchester
 Martin Rinard        Massachusetts Institute of Technology
 Mark Stickel         SRI International

WORKSHOPS, TUTORIALS, SYSTEM COMPETITIONS:
 There will be a two-day programme of eight workshops and four
 tutorials before the conference. In addition, two system
 competitions will be held during the conference.

   Workshops:
     o Automated Deduction: Decidability, Complexity,
           Tractability (ADDCT)
     o Beyond SAT: What About First-Order Logic?
     o Logical Frameworks and Meta-Languages: Theory and
           Practice (LFMTP)
     o Modules and Libraries for Proof Assistants (MLPA)
     o Proof Search in Type Theories (PSTT)
     o Satisfiability Modulo Theories (SMT)
     o The International Workshop on Unification (UNIF)
     o TPTP World Workshop (TPTPWoWo)

   Tutorials:
     o Hierarchical and Modular Reasoning in Complex Theories
     o Probabilistic Analysis Using a Theorem Prover
     o Precise, Automated and Scalable Verification of Systems
           Software Using SMT solvers
     o Logics with Undefinedness

   System competitions:
     o The CADE ATP System Competition (CASC)
     o Satisfiability Modulo Theories Competition (SMT-COMP)

 Details will be published in separate calls and on the
 conference website.

STUDENT AWARDS
 Travel awards will be available to enable selected students to
 attend the conference. Details will be published on the
 conference website.

PUBLICATION DETAILS:
 The proceedings of the conference will be published in the
 Springer LNAI/LNCS series.

SUBMISSION INSTRUCTIONS:
 Submissions can be made in the categories 'regular papers' and
 'system descriptions'. The page limit in Springer LNCS style is
 15 pages for regular papers and 5 pages for system
 descriptions. Full system descriptions that provide in-depth
 presentation of original ideas in an implemented system can be
 submitted as regular papers. For the benefit of reviewers,
 additional material may be provided by a clearly marked
 appendix or a reference to a manuscript on a website. It is at
 the discretion of the reviewers whether such supplements will
 be considered. All regular papers will be evaluated according
 to the highest standards in terms of originality, significance,
 technical quality, and readability.

 Submissions must be in English and standard conforming pdf
 format. Submissions must be unpublished and not submitted for
 publication elsewhere. Authors are strongly encouraged to
 produce their papers in LaTeX.

 Formatting instructions and the LNCS style files can be
 obtained via http://www.springer.de/comp/lncs/authors.html.

To submit your paper please use the EasyChair submission system
at this address:
http://www.easychair.org/conferences/?conf=cade22.


IMPORTANT DATES:
A paper title and a short abstract of about 100 words must be
submitted before the paper.


     16  Feb 2009 Abstract submission deadline
     23  Feb 2009 Paper submission deadline
     10  Apr 2009 Notification of paper decisions
     14  May 2009 Camera-ready papers due

     2-3 Aug 2009 Workshops & Tutorials
     4-7 Aug 2009 Conference, including CASC and SMT-COMP

PROGRAM COMMITTEE:
Alessandro Armando Università di Genova
Franz Baader Technische Universität Dresden
Peter Baumgartner NICTA, Canberra
Maria Paola Bonacina Università degli Studi di Verona
Bernhard Beckert Universität Koblenz-Landau
Nikolaj Bjørner Microsoft Research
Alessandro Cimatti Istituto per la Ricerca Scientifica e Tecnologica, Trento
Silvio Ghilardi Università degli Studi di Milano
Jürgen Giesl RWTH Aachen
Rajeev Goré The Australian National University
Reiner Hähnle Chalmers University of Technology
John Harrison Intel Corporation
Miki Hermann École Polytechnique
Ullrich Hustadt University of Liverpool
Katsumi Inoue National Institute of Informatics, Japan
Tommi Junttila Helsinki University of Technology
Deepak Kapur University of New Mexico
Alexander Leitsch Technische Universität Wien
Christopher Lynch Clarkson University
Claude Marché INRIA Saclay, Parc Orsay Université
William McCune University of New Mexico
Aart Middeldorp Universität Innsbruck
Hans de Nivelle University of Wroclaw
Albert Oliveras Universitat Politècnica de Catalunya
Lawrence Paulson University of Cambridge
Brigitte Pientka McGill University
David Plaisted University of North Carolina at Chapel Hill
Michaël Rusinowitch LORIA-INRIA-Lorraine
Renate Schmidt (Chair) The University of Manchester
Carsten Schürmann IT-Universitetet i København
Aaron Stump The University of Iowa
Geoff Sutcliffe University of Miami
Cesare Tinelli The University of Iowa
Andrei Voronkov The University of Manchester
Christoph Weidenbach Max-Planck-Institut für Informatik


ORGANIZERS:
Conference Chair: Brigitte Pientka McGill University
Workshop & Tutorial Chair: Aaron Stump The University of Iowa
Publicity Chair: Carsten Schürmann IT-Universitetet i København
PC Chair: Renate Schmidt The University of Manchester