[SMT-COMP] SMT-COMP 2007 -- call for suggestions

[Roberto Sebastiani]

A few comments/suggestions:

On Fri, 9 Mar 2007, Albert Oliveras Llunell wrote:

> Dear colleagues,
>
> As you probably know, SMT-COMP'07 will take place next July in
> collocation with CAV at Berlin. As was done last year, before
> posting the official rules for this edition we would like to receive
> as many suggestions as possible from participants and other people
> interested in the event. We will collect suggestions until March 18,
> at which point we will start defining the rules for the next edition.
>
> Although all suggestions are welcome, here we outline some potentially
> interesting topics:
>
> - Requirements for a solver to enter the competition: an interesting
> point concerns the submission of solvers that, after some
> preprocessing, call other SMT solvers. Last year's policy was that
> an SMT solver could be used in this fashion only if it was from last
> year's edition and permission was given by the authors of the solver.

I also propose that, in this case, the name of the external solver should be 
explicitly mentioned: <solver> ==> <solver>+<external solver>
E.g., considering an example for last year: HTP ==> HTP+Barcelogic1.0.

I also wonder wether it makes any sense to classify a tool which worsens the 
performances of the external SMT tool used. Therefore, I propose to disregard 
any such tool which does not perform better than the tool  used 
as an external device.


>
> - Technical setting of the competition: number of benchmarks executed,
> time given for benchmark, distribution among industrial / crafted
> /random benchmarks, punctuation system, disqualification policy,
> addition/deletion of a division, scrambling, ...
>
> - Organizational details: format of the presentation session at
> SMT'2007, awards (to solvers and maybe even to benchmark submissions,
> as is done in the SAT competition), timeline, display of real-time
> results, ....

I propose to make a special award for the best-performing new-entry solver
(which is not the new name or a reimplementation of a previous one).

Roberto


>
>
> Best wishes,
> Albert, for Aaron and Clark too.
>
>
>
>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>

-- 
------------------------------------------------------------------
Prof. ROBERTO SEBASTIANI
Dip. Informatica e Telecomunicazioni
Fac. Scienze M.F.N., Universita` di Trento    Tel: +39 0461 881514
Via Sommarive 14, I-38050, Trento, Italy      Fax: +39 0461 882093
roberto.sebastiani at dit.unitn.it     http://www.dit.unitn.it/~rseba
------------------------------------------------------------------