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.
- New decision procedures
- New methods of implementing decision procedures
- New ways of using of the infrastructure common to decision procedures
- Applications and case studies
- 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.
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.
Notification of acceptance/rejection: June 23rd, 2006 (MODIFIED!)
Camera-ready copies due: July 3rd, 2006 (MODIFIED!)
Workshop: August 21st, 2006
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.
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.
Accepted papers, final program and slides of the talks
A list of all presentations with the slides of the talks is available here
Registration and local information