PDPAR'03

Pragmatics of Decision Procedures in Automated Reasoning 2003
You can download the whole text as a PDF file or you can look at the workshop program to download each signle paper (in gzipped postscript format).

Workshop Program

Call for papers (in plain text)

















A workshop affiliated to CADE 19
July 29, 2003
Miami
USA

























Workshop Program























Background

 Decision procedures for the validity or the satisfiability problem of fragments of first-order logic or other logics are considered as key ingredients to provide an adequate degree of automation in any formal verification efforts.

In the literature, three aspects of decision procedures have received and still receive great attention:

  1. designing decision procedures for certain decidable fragments,
  2. combining decision procedures for two theories T1 and T2 to build a decision procedure for a suitable combination of T1 and T2, and
  3. integrating decision procedures into more general reasoning activities, such as rewriting, boolean reasoning, and so on.
In contrast, little or no attention has been paid so far to the more concrete issues of

implementing and testing

the effectiveness of decision procedures. This state of affairs has prevented the exchange of architectural and implementation techniques as well as the creation of a library of benchmarks on which to compare the performances of systems in a sensible way. This is a major obstacle for implementors of reasoning systems to re-use the cornucopia of algorithms, combination, and integration schemes that have been implemented in state-of-the-art reasoning systems. However, there is a growing interest in these issues as witnessed by the SMT-LIB initiative (Satisfiability Modulo Theories Library). The initiative aims at establishing a library of benchmarks for formula satisfiability w.r.t. to background theories for which decision procedures existq, such as the theory of lists, of arrays, linear arithmetic, and so on.



























































Goals & Topics

The workshop has two main goals.

The first is to bring together people interested in the pragmatical aspects of decision procedures in automated reasoning, giving them a forum for presenting and discussing implementation and evaluation techniques.

The second is to provide a discussion forum for the SMT-LIB initiative. At the moment, an SMT-LIB interest group, coordinated by the proponents of this workshop, is working on a common standard for the specification of benchmarks and background theories. The workshop will host panel discussions aimed at finalizing the SMT-LIB common format.

Topics of interest include (but are not limited to)












































































Audience

 The intended audience of the workshop is implementors and expert users of automated reasoning systems, people interested in any field in which decision procedures have a predominant role, such as automated verification, planning and scheduling, compiler optimization, and so on.

























































































Format

 The workshop is meant to be an opportunity both to form a community of people interested in the pragmatics of decision procedures and to discuss the issues related to the SMT-LIB initiative. We intend to have invited talks, sessions with contributed talks (20 minutes + 10 minutes for questions), as well as panel discussions on the SMT-LIB format. Attendance will be open.

























































































Call for abstracts

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

Topics of interest include (but are not limited to)

Another goal of the workshop is to provide a discussion forum for the SMT-LIB initiative, a research initiative aimed at establishing a common standard for the specification of benchmarks and background theories for satisfiability modulo theories, and at creating a repository of such benchmarks. (See http://combination.cs.uiowa.edu/smtlib/ for more info.)

The workshop will host panel discussions on the SMT-LIB format.

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 pdpar03@cs.uiowa.edu and contain:

  1. title, author(s) (names, correspondence addresses, e-mail addresses), and abstract of no more than 300 words in plain text;
  2. the abstract in postscript or PDF format, as an attachment;
  3. a single file with the LaTeX2e source of the abstract, including any non-standard macro used, again as an attachment.
Submissions will be peer-reviewed. The authors of accepted submissions are expected to give a 25' presentation at the workshop. The proceedings of PDPAR'03 will be published as an INRIA technical report, and will be distributed at the workshop.

























































































Important Dates

























































































Program Committee

























































































Registration

 Joint registration with the CADE-19 conference is possible but is not required.

Refer to the CADE-19 web site for registration instructions and deadlines.

























































































Related Links