Call for Papers

Pragmatics of Decision Procedures in Automated Reasoning

PDPAR'05

July 12, 2005 -- The University of Edinburgh, Scotland, UK

PDPAR'05 is an affiliated workshop to CAV'05.

Background

Both the Formal Verification community and the Automated Reasoning community have long recognised the importance of decision procedures for the validity or the satisfiability problem of fragments of first-order logic.

In Formal Verification, many interesting and powerful decision procedures have been developed, and applied to the verification of word-level circuits, hybrid systems, pipelined microprocessors, and software. The Automated Reasoning community, on the other hand, has primarily focussed on the principles underlying the design and combination of decision procedures for different decidable theories, and on their integration into more general reasoning activities (e.g. rewriting, boolean reasoning).

Limited attention has been paid so far to the concrete issues of implementing and assessing the effectiveness of decision procedures. This state of affairs has so far prevented the exchange of architectural solutions and implementation techniques. Furthermore, the lack of a common library of benchmarks on which to compare the performances of systems in a systematic way has so far made it difficult to compare and evaluate experimentally the merits of the different techniques.

Topics

The main goal of this workshop is to bring together researchers interested in the pragmatical aspects of decision procedures, giving them a forum for presenting and discussing implementation and evaluation techniques.

Topics of interest for the workshop include (but are not limited to):

The workshop will also serve as a forum for the development of the Satisfiability Modulo Theories Library (SMT-LIB) initiative, that aims at establishing a library of benchmarks of practical relevance for different theories in a standardized language.

The methodology and the results of the "Satisfiability Modulo Theories Competition" (SMT-COMP) will be presented and discussed in a special session of the workshop. The workshop will host panel discussions on the SMT-LIB and SMT-COMP initiatives.

Paper Submissions

Extended abstracts addressing the pragmatical aspects of decision procedures are solicited. Submitted abstracts should not exceed 8 pages and should be written in LaTeX with the following settings: 11pt, one column, a4paper and standard margins.

Submissions should be sent by email to pdpar05 _at_ ai.dist.unige.it and contain:

  1. title, author(s) (names, correspondence addresses, e-mail addresses);
  2. small abstract (< 300 words), in plain text;
  3. extended abstract in postscript or PDF format, as an attachment;
Submissions will be reviewed by at least to referees. The authors of accepted submissions are expected to give a 25' presentation at the workshop. The proceedings of PDPAR'05 will be be distributed at the workshop.

Registration

Joint registration with the CAV'05 conference is possible but is not required. Refer to the CAV'05 web site for registration instructions and deadlines.

Invited Speakers

Important Dates

Program Committee

Organizers

Links

PDPAR'05 is sponsored by:

Microsoft Research