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:

Submissions

Full paper submissions should be at most 12 pages in EasyChair LaTeX format (available here), although shorter papers are welcome. Position statements about "solution quality", of up to 5 pages, are also invited. Submission is via the EasyChair system.

Important Dates

Submission deadline:  April 12
Notifications: April 28
Final version: May 17
Workshop date: July 20, 2010

Invited Speakers and Panelists

Organizers

Program Committee

Program

In addition to talks on original and previously presented research, the program will include a panel on the main topics on the workshop, with an emphasis on solver competitions and solver community infrastructure, followed by a facilitated discussion on quality metrics for solver solutions.

09:00-10:00 Joe Hurd.
Evaluation Opportunities in Mechanized Theories (invited talk)
10:00-10:30 Coffee break
10:30-11:00 Robert Brummayer, Aaron Stump and Duckki Oe.
Exploring Predictability of SAT/SMT Solvers
11:00-11:30 Claudia Peschiera, Luca Pulina and Armando Tacchella.
Designing a solver competition: the QBFEVAL'10 case study
11:30-12:00 Mladen Nikolic.
Statistical Methodology for Comparison of SAT Solvers (presentation-only)
12:00-12:30 Christoph Benzmueller and Marvin Schiller.
Adaptive Assertion-Level Proofs
12:30-14:00 Lunch break
14:00-14:30 Morgan Deters.
The SMT-Exec Execution Service: Features, Fairness, and the Future (presentation-only)
14:30-15:00 Geoff Sutcliffe, Cynthia Chang, Li Ding, Deborah McGuinness and Paulo Pinheiro da Silva.
Different Proofs are Good Proofs (position statement)
15:00-15:30 Coffee break
15:30-16:15 EMS panel on solver competitions and community infrastructure (shared with SVARM)
16:15-17:00 QMS facilitated discussion on quality metrics

Support

The workshop is partially supported by a planning grant from the National Science Foundation. Any opinions, findings and conclusions or recommendations expressed here are those of the organizers and do not necessarily reflect the views of funding agency.

































Q
EMS
S
 2010

Background

Call for papers

Submissions

Important Dates

Invited Speakers

Organizers

Committee

Program

Support