Logic List Mailing Archive
3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'05), Edinburgh July 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
======================================================================
*****************************************************
*** SUBMISSION DEADLINE APPROACHING: 9 April 2005 ***
*****************************************************
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: 9 April 2005
Notification of acceptance: 14 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@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.
Informal proceedings will be available at the workshop and be
published on-line on the workshop's web page at
http://www.ai.dist.unige.it/pdpar05/
------------
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.