paper on HWMCC 2014

[Gianpiero Cabodi]

To all HWMCC2014 participants.

As you might have noticed from previous emails, we are considering a paper on HWMCC 2014, for submission to the JSAT special issue on CAV & FLoC 2014 competitions (http://satcompetition.org/2014/cfp.shtml). 

After discussing the issue with Armin Biere (organiser) and Jason Baumgartner (contributor of the largest (6s*) benchmark set), we're planning to work at a paper with some (very limited) or no experimentation (just if necessary, due to the nov 14th deadline), and a discussion on tools/benchmarks, possibly limited to: (i) brief descriptions of tools; (ii) postprocessing & comparative analysis of HWMCC’14 publicly available results.

So we're thinking about a paper where we’ll first (and quickly) collect some data from authors of all HWMCC tools.

We plan to start our work from Armin Biere’s analysis (results and slides) on HWMCC’14 and previous editions, to be integrated by extra data from authors.

Authors are thus invited to send a brief description of their tool, with details and comments they may deem relevant, based on the template which follows. This is particularly important this year, as Armin did not solicit tool descriptions as usual, due to time constraints of the competition presentation at CAV’14. For authors that will not answer, we'll provide a brief tool description based on available data.

We'll also work at a comparison among different tools. based on benchmark-tool coverage matrices (generated from HWMCC’14 data), and/or any available extra data/description from authors.

Though still a partial work, the main aim of the paper is to provide a better insight on HWMCC tools and benchmarks, for both an academic and an industrial audience. Though we're aware that more experimental work would be required for a solid/stronger tool/benchmark characterisation, this could definitely represent an initial step. We’re also aware that a scientifically sound evaluation is difficult/impossible, we’ll thus limit our discussion to empirical observations.

Since we have very tight deadlines, I will coordinate the paper setup with my colleague Stefano Quer. The paper will be co-authored by Armin Biere and Keijo Heljanko (as HWMCC’14 organisers), Jason Baumgartner (for a description the “6s” benchmark set), and some PhD students in our group, who will take care of practical issues (e.g. direct interactions with tool authors, analysis of data, data preparation) and paper editing. 

Any comment is welcome, as soon as possible. 

Best, 

Gianpiero

Template for author feedback follows. 

If interested, please fill it and send feedback to:

stefan...@polito.it

Direct interactions with those of you who will answer will then be handled by students in our group.

——————————————————————————————————————————————————————————————

(cut here, edit and email to stefan...@polito.it)

HWMCC’14 tool description

- tool name, authors & organisation

- publication reference(s) (for tool citation)

- tool description

  + code, language, integration of external tools

  + main MC engines (e.g. IC3, BMC, interpolation, etc.)

  + transformations used (e.g. signal/latch correspondence, retiming, phase abstraction, etc.)

  + portfolio organisation 

     - how and when engines are run

     - single thread vs. multiple processes/threads (concurrency model, communcation)

     - expert system or top level scripting strategies: efforts, time-out, etc.

- general comments on the HWMCC'14

  + tool targets, i.e., sat/unsat instances, easy/hard, deeper/shorter bounds

  + run times, memory behavior, etc.  

  + detailed results, e.g., which techniques were the reason for success on certain benchmarks (particularly interesting for "unique wins")

  + expectation versus final results, e.g., results were as expected, there were problems, they could have been better, etc.

- any further comment the Authors would like to highlight