[SMT-COMP] SMT-COMP 2015: Call for Comments, Benchmarks, Solvers

[Mate Soos]

Hey All,

Newbie here so please take the stuff below with a pinch of salt. Sorry.

On 02/08/2015 04:18 PM, Tjark Weber wrote:
> - Sequential vs. parallel performance: All solvers will have several
> CPU cores available, and we plan to measure CPU and wall time. Solver
> developers might wish to prepare both sequential and parallel versions
> of their solvers.

So there will be 2 tracks, one parallel one sequential? How many CPU
cores for the parallel? 2? 16? 32? Memory limit should probably be
higher for the parallel? Or not?

Along the same lines: what timeout will there be? Wall clock timeout for
parallel I guess? How will perf be compared for parallel? sum(cpu
time)/numcpu or wall-clock time? If there is contention on locked stuff
these may be very different. Also, if I decide to use only 10 of 16
cores (due to mem limit), they are different again.

Further, roughly what timeouts are planned to be used (i.e. how many
minutes)? Maybe there could be 2 tracks, one with shorter one with
longer timeouts? (naturally, only needs to run 1x but would deal out 2
awards) Some users are very time-conscious (10s is much too long), some
are not (10 minutes is fine).

> - Benchmark selection: We will likely have sufficient computational
> resources to run all solvers on all eligible benchmarks. Therefore, we
> are interested in proposals for weighing the results so as to avoid
> over-representation of certain (large) benchmark families.

I think there are some users of symbolic execution tools who have nice
examples. Fuzzing has exploded in the past couple of years, maybe there
are some interesting examples out there. I'm forwarding to some people
(John Regehr, Stephen McCamant, Xi Wang), maybe others can fw to more.

Looking forward to the comp, thanks for organizing it!

Mate


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-comp/attachments/20150318/bf4766ba/attachment.asc>