[TYPES] PDPAR'05: Submission deadline extended to April 18, 2005

[Alessandro Cimatti]

***********************************************************
*** NEW: SUBMISSION DEADLINE EXTENDED TO APRIL 18, 2005 *** 
***********************************************************

======================================================================

                             CAV'05 Workshop

                     3rd Workshop on Pragmatics of
               Decision Procedures in Automated Reasoning
                               (PDPAR'05)

   	          http://www.ai.dist.unige.it/pdpar05/

                         Edinburgh, Scotland, UK
                              July 12, 2005

                             CALL FOR PAPERS

======================================================================


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
performance  of  systems  in a  systematic  way  has  so far  made  it
difficult  to compare and  evaluate experimentally  the merits  of the
different techniques.

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):

* algorithms and data structures to implement decision procedures,
* techniques for the rapid prototyping of decision procedures,
* techniques to implement combination or incorporation schemes,  
* benchmarks to evaluate and/or to compare decision procedures,
* methodologies to assess the effectiveness of decision procedures,
* the role of decision procedures in real-world verification efforts,
  and  
* techniques for promoting the re-use and the exchange of code
  implementing decision procedures, combination and integration 
  schemes, and so on.

The workshop  will also serve  as a forum  for the development  of the
"Satisfiability    Modulo    Theories    Library"    (SMT-LIB,    URL:
http://combination.cs.uiowa.edu/smtlib)   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.

---------------
Important Dates
---------------

Submission deadline: 18 April 2005
Notification of acceptance: 18 May 2005
Final versions: 11 Jun 2005
Workshop: 12 July 2005

-----------
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 two referees. The authors of
accepted submissions  are expected to  give a 25' presentation  at the
workshop.   

Accepted contributions will be be published in a special volume of the
Electonic Notes in Theoretical Computer Science ENTCS.  

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

-----------------
Program Committee
-----------------

Alessandro Armando (University of Genova, Italy) [Co-chair]
Alessandro Cimatti (IRST, Trento, Italy) [Co-chair]

Thomas Ball (Microsoft Research)
Clark Barrett (New York University, USA)
Randy Bryant (Carnegie-Mellon University, USA)
David Dill (Stanford University, USA)
Enrico Giunchiglia (University of Genova, Italy)
Predrag Janicic (University of Belgrade,  Serbia and Montenegro)
Greg Nelson (HP Labs, USA)
Silvio Ranise (INRIA-Lorraine, France)
Harald Ruess (SRI, USA)
Roberto Sebastiani (University of Trento, Italy)
Eli Singerman (Intel)
Ofer Strichman (Technion - IIT, Israel)
Aaron Stump (Washington University, USA)
Cesare Tinelli (University of Iowa, USA)

----------------
More Information
----------------

See http://www.ai.dist.unige.it/pdpar05 for PDPAR'05, and
http://www.cav2005.inf.ed.ac.uk/ for CAV'05.