Decision procedures are key components within many formal verification and automated reasoning tools. Their performance, capacity, and scalability are vital to the tools that depend on them. Furthermore, new extensions may allow the formal verification or automated reasoning tools to use decision procedures more effectively.

The goal of PDPAR is to bring together researchers interested in both the theoretical and the pragmatical aspects of decision procedures, giving them a forum for presenting and discussing not only theoretical and algorithmic issues, but also implementation and evaluation techniques, with the ultimate goal of making new decision procedures possible and old decision procedures more powerful and more useful.

PDPAR topics bridge the automated reasoning and formal verification communities. Sample topics of interest include (but are not limited to):

• New decision procedures
• New methods of implementing decision procedures
• New ways of using of the infrastructure common to decision procedures
• Applications and case studies

PDPAR'06 will accept two types of papers:

• Original papers: should describe original research and contain sufficient detail to assess the merits and relevance of the contribution. Simultaneous submission of material is prohibited. Given the informal style of the workshop, the submission of papers presenting student's work and work in progress is encouraged.
• Presentation-only papers: describe work previously published in non-FLOC'06 forums, and will *not* be inserted in the proceedings. We are allowing the submission of previously published work in order to allow researchers to communicate good ideas that the PDPAR attendees are potentially unaware of.

Both kind of submissions will be reviewed by at least two referees, possibly more.
Submissions should be made via Easychair (much preferred) or sent by email to pdpar06[AT]dit.unitn.it (substitute [AT] with "@"). In the latter case, it should include:

• the paper in PDF (preferred) or PostScript format as an attachment. The paper should not exceed 10 pages, including the bibliography, and should be written in LaTeX with the following settings: 11pt, one column, a4paper and standard margins. The paper may include, in addition, an appendix containing technical details, which reviewers may read or not, at their discretion;
• a submission message, with names and affiliations of all authors, the title of the paper, the contact author's postal and e-mail addresses phone number, and a one- or two-paragraph abstract, and the type of submission.

Given the informal style of the workshop, only informal (non-archival) proceedings will be distributed at the workshop. A selected subset of the submitted papers will be published as post-proceedings in a special volume of the Electronic Notes in Theoretical Computer Science (ENTCS) (unless the authors prefer not to).

Submissions due: May 15th, 2006
Notification of acceptance/rejection: June 23rd, 2006 (MODIFIED!)
Camera-ready copies due: July 3rd, 2006 (MODIFIED!)
Workshop: August 21st, 2006

Speaker: Koen Claessen, Chalmers University and Jasper Design Automation.
Title: The Power of Finite Model Finding
Abstract: Paradox is a tool that automatically finds finite models for first-order logic formulas, using incremental SAT. In this talk, I will present a new look on the problem of finding finite models for first-order logic formulas. In particular, I will present a novel application of finite model finding to the verification of finite and infinite state systems; here, a finite model finder can be used to automatically find abstractions of systems for use in safety property verification.
In this verification process, it turns out to be vital to use typed (or sorted) first-order formulas. Finding models for typed formulas brings the freedom to use different domain sizes for each type. How to choose these different domain sizes is still very much an unexplored problem. We show how a simple extension to a SAT-solver can be used to guide the search for typed models with several domains of different sizes.

Speaker: Peter O'Hearn, Queen Mary, University of London
Title: Proof Procedures for Separated Heap Abstractions
Abstract: Separation logic is a program logic geared towards reasoning about programs that mutate heap-allocated data structures. This talk describes ideas arising from joint work with Josh Berdine and Cristiano Calcagno on proof procedure for a sublogic of separation logic that is oriented to lightweight program verification and analysis. The proof theory uses ideas from substructural logic together with induction-free reasoning about inductive definitions of heap structures. Substructural reasoning is used to to infer frame axioms, which describe the portion of a heap that is not altered by a procedure, as well as to discharge verification conditions; more precisely, the leaves of failed proofs can give us candidate frame axioms. Full automation is achieved through the use of special axioms that capture properties that would normally be proven using by induction.
I will illustrate the proof method through its use in the Smallfoot static assertion checker, where it is used to prove verification conditions and infer frame axioms, as well as in the Space Invader program analysis, where it is used to accelerate the convergence of fixed-point calculations.

The list of accepted papers and the final program can be found at Floc'06 PDPAR page .

A list of all presentations with the slides of the talks is available here

Information about registration, and the workshop's location is available at the FLoC 2006 website.

Online copies of the informal proceedings are available here.

PDPAR'06 gratefully acknowledges the financial support from