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.