PDPAR'04

Second Workshop on Pragmatics of Decision Procedures in Automated Reasoning 2004


Workshop program available with pdf files of contributions


A workshop affiliated to IJCAR 2004
July 05, 2004
University College Cork
Cork, County Cork, Ireland

























Workshop Program

[to be announced]























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 attention has been paid so far to the more concrete issues of implementing and testing the effectiveness of decision procedures.

PDPAR was established in 2003 as a forum for discussing these issues, foster the exchange of architectural and implementation techniques, as well as support the creation of large benchmarks collections for comparing the performances of systems in a sensible way.
For the latter, PDPAR also serves as a discussion outlet for the SMT-LIB initiative, an international initiative aimed at establishing a common library of benchmarks for satisfiability modulo theories.





























































Goals & Topics

The workshop has two main goals.
  1. 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.
  2. The second is to provide a discussion forum for the SMT-LIB initiative. The workshop will host a panel discussion aimed at discussing the SMT-LIB common format and the other organisational aspects of handling the library.
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.

























































































Call for abstracts

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 pdpar04@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.

    IMPORTANT! In order to ease the (possible) publication in the ENTCS volume of the workshop proceedings, please, use the following LaTeX header in your submission:

    \documentclass[a4paper,11pt]{article}
    \textwidth 14.63cm
    \textheight 22cm
    \oddsidemargin 0.65cm
    \evensidemargin 0.65cm
    \topmargin 0.55cm
    \headheight 0.0pt
    \headsep 0.0pt

Submissions will be peer-reviewed. The authors of accepted submissions are expected to give a 25' presentation at the workshop. The proceedings of PDPAR'04 will be distributed at the workshop and later published as an INRIA technical report or possibly as a special volume of the Electronic Notes in Computer Science (ENTCS).

























































































Important Dates

Please, notice the new extended deadline!

























































































Program Committee

























































































Registration

 Joint registration with the IJCAR 2004 conference is possible but is not required.

Refer to the IJCAR 2004 web site for registration instructions and deadlines.

























































































Related Links