******************************************************************************
                  ==================================
                  Call for Papers - Revised Timeline
                  ==================================

                            The Workshop on 
   Evaluation Methods for Solvers and Quality Metrics for Solutions
                    http://clc.cs.uiowa.edu/EMSQMS/

                     20th July 2010, Edinburgh, UK

                            Affiliated with 
 IJCAR 2010, the 5th International Joint Conference on Automated Reasoning
 CAV 2010, the 22nd International Conference on Computer Aided Verification 

******************************************************************************
Background
----------
Logic solvers, e.g., first-order ATP systems, SMT systems, SAT solvers, 
higher-order proof assistants, are valuable tools in a growing range of 
applications, e.g., mathematics, software and hardware verification, 
knowledge based reasoning, etc. A key to progress in the development of 
high-performance logic solvers is their evaluation. Meaningful evaluation 
is dependent on various components: appropriate benchmark problems, 
execution in the context of comparable resources, careful analysis of the 
output data, and so on. Most solver communities support each of these in 
various ways.

A survey of the evaluation approaches in the various solver communities 
shows that there is a large emphasis on the ability to solve problems, a 
moderate emphasis on the resources required to find those solutions, but 
only a small emphasis on the quality of the solutions. There is however a 
strong interest by users in solution quality, starting most formally at the 
correctness of solutions output, but extending to notions of compactness,
readability, etc.  

Aims and Scope
--------------
The EMSQMS workshop is concerned with the aspects of logic solver evaluation 
described above: methods by which logic solvers can be meaningfully 
evaluated, with a separated focus on metrics by which solvers' solutions 
can be evaluated. The workshop will collect ideas and inputs on these 
topics, to provide specific advice and resources that will help logic 
solver developers and users obtain meaningful evaluations for research 
and application.

Topics (include, but are not limited to)
------
-- evaluation methods for logic solvers: 
  -- benchmarking frameworks,
  -- solver execution services,
  -- solver competitions,
  -- techniques for checking solver soundness, including solver 
     debugging techniques.

-- quality and comparison metrics for solvers' solutions (proofs, models, and
  other artifacts):
 -- correctness,
 -- conciseness,
 -- readability,
 -- portability,
 -- novel metrics.

Submissions
-----------
Full paper submissions should be at most 12 pages in EasyChair format
(available from the EMSQMS web page http://clc.cs.uiowa.edu/EMSQMS/), though 
shorter papers are welcome. Position statements about "solution quality", 
of up to 5 pages, are also invited. Submission is via the EasyChair system:

   http://www.easychair.org/conferences/?conf=emsqms2010

Dates
-----
Submission deadline: 12th April
Notifications: 28th April
Final version: 17th May

Program Committee
-----------------
Christoph Benzmueller, Articulate Software
Armin Biere, Johannes Kepler University
Li Ding, Rensselaer Polytechnic Institute
Daniel Le Berre, Universite d'Artois
Deborah McGuinness (co-organizer), Rensselaer Polytechnic Institute
Adam Pease, Articulate Software
Paulo Pinheiro da Silva, University of Texas at El Paso
Ulrike Sattler, The University of Manchester
Torsten Schaub, University of Potsdam
Aaron Stump (co-organizer), The University of Iowa
Geoff Sutcliffe (co-organizer), University of Miami
Armando Tacchella, Universita di Genova
Cesare Tinelli (co-organizer), The University of Iowa

******************************************************************************