[SMT-LIB] your feedback on the future of SMT-COMP

[Viktor Kuncak]

Dear Cesare and the Steering Committee

First of all, as mostly a user (and contributor at conceptual level)
of SMT technology, I am very grateful for the competition and its
impact, as well as everyone who kept it running!

The barrier to entry is perhaps high because the problem is so
difficult: it has expectations of expressive power and efficiency that
do not exist in any other domain.

Having an up-to-date evaluation of current SMT solvers on an evolving
set of benchmarks is certainly valuable in my point of view. From your
description it seems to me that SMT-EVAL would do this job well, so I
support it.

In the longer term, I am thinking that it would be good to automate
the process as much as possible, make it easy to repeat evaluations
anywhere, with any subset of benchmarks and solvers, so that
evaluation becomes a collective effort that will run by itself in the
stable state. At some point, paper submissions can be expected to
perform such evaluations and make it easy for reviewers and readers to
reproduce the evaluations, with results and artifacts stored for
future reference.

In terms of the applications, SMT is as relevant as ever, but what
would make it even more relevant if we make it possible to use it to
faithfully represent software in a way that makes it possible to run
it and verify it using SMT-LIB as the format. Even though this is just
one possible application, if you envision for a moment a serious
software package or an OS that ships with SMT-LIB files accompanying
all executables, this would give SMT-LIB a whole new dimension. Such
goals have been a part of our agenda in the "Rich Model" activity,
richmodels.org, http://richmodels.org/ (next meeting runs along VMCAI
at POPL 2013 in Rome) and it is recently that I have started to
realize just how close SMT-LIB is to already being able to serve such
purpose.

To make SMT-LIB work for software verification and certification,
there is essentially no change in format required. What we need to
accept is the idea that we can prove satisfiability for *quantified*
formulas with uninterpreted predicates. A certificate of
satisfiability maps uninterpreted predicates into formulas in
decidable axiomatized theories (such as linear arithmetic and finitely
generated arrays).  Typically the predicates will be defined as Horn
clauses, but this is not required from the problem definition point of
view. Such satisfiability checking subsumes problems such as invariant
generation, and I believe it is a very exciting development. I am not
implying that any of these are my ideas, others on these lists have
done more and understood them long ago. I am excited that this
folklore is becoming more popular, because it can really be a game
changing direction in terms of practical impact, and the current SMT
lib and its evaluation are the best starting point we have.

Best regards,

  Viktor

On Wed, Nov 21, 2012 at 9:22 AM, Tinelli, Cesare
<cesare-tinelli at uiowa.edu> wrote:
> Dear members of the SMT community,
>
> The Steering Committee of the SMT workshop, which is also in charge of appointing the organizers of SMT-COMP, seeks your input on the future of the competition.
>
> Two of the SMT-COMP organizers, Roberto Bruttomesso and Alberto Griggio, are stepping down this year, at the end of their two-year appointment. They have both been asked and have agreed to chair SMT'13, and so are not in a position to co-organize the next SMT-COMP.
> While the other organizer, David Cok, is willing to continue for another year with the help of new partners, this seems like a good time to reassess SMT-COMP and discuss its future.
>
> Although the benefits of SMT-COMP to the fields are undeniable, it appears that after 8 years a certain level of fatigue and diminished enthusiasm has set in. The barriers to entry for new solvers seems as high as they have ever been. Even for some established solvers and their developers participation in the competition has become quite onerous and offers unclear rewards, for a number of reasons.
>
> So we would like to hear from you, and in particular of course from SMT solver developers, about whether we should
>
> - continue with SMT-COMP or not in the first place,
> - keep it as an annual event or perhaps make it biennial and,
>   if so, starting when,
> - change the format, the focus, or any other aspect of the competition
>   to make it more attractive/relevant/etc. to participants or "spectators".
>
> Your feedback on this as well as expressions of interest in becoming an SMT-COMP organizer would be greatly appreciated.
>
> Thanks,
>
>
> Cesare, for the SMT SC
>
>
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib



-- 
Viktor Kuncak
http://lara.epfl.ch/~kuncak

A reminder:
http://grad-schools.usnews.rankingsandreviews.com/best-graduate-schools/top-science-schools/computer-science-rankings