Re: [Smtcomp-discussion] [SMT-LIB] SMT-COMP 2015: Call for Comments, Benchmarks, Solvers
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
From: Dejan J. <dej...@gm...> - 2015-05-04 18:41:14
|
On Sun, Feb 8, 2015 at 7:20 AM Tjark Weber <tja...@it...> wrote: > ====================================================================== > > 10th International Satisfiability Modulo Theories Competition > (SMT-COMP'15) > > July 19, 2015 > San Francisco, USA > > CALL FOR COMMENTS > CALL FOR BENCHMARKS > PRELIMINARY CALL FOR SOLVERS > > ====================================================================== > > SMT-COMP is the annual competition among Satisfiability Modulo Theories > (SMT) solvers. The goals of SMT-COMP are to spur solver advances, > collect benchmarks, and encourage adoption of the SMT-LIB standard, > through friendly competition. > > SMT-COMP'15 will end in time to be described and the results announced > at the SMT Workshop (July 18-19), which is affiliated with the 27th > International Conference on Computer Aided Verification (CAV 2015). > > SMT-COMP'15 is organized under the direction of the SMT Steering > committee. The organizing team for SMT-COMP'15 is > > . Sylvain Conchon - Paris-Sud University, France > . David Deharbe - Federal University of Rio Grande do Norte, Brazil > . Tjark Weber - Uppsala University, Sweden > > This is a call for three things: > > CALL FOR COMMENTS: > > The organizing team is preparing the schedule and rules for 2015. > Any comments you may have to improve the competition over past years > or to redirect its focus are welcome and will be considered by the > team. Please submit such comments by *** 22 February 2015. *** > > For SMT-COMP'15, we are particularly interested in comments regarding: > > - 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. > > - 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. > > - Scope: After the successful migration to StarExec in 2013/14, we are > considering to broaden the scope of SMT-COMP again. We might reinstate > additional tracks, e.g., for unsat core extraction and proof-producing > solvers. > > CALL FOR BENCHMARKS: > > The competition is enhanced by new sets of benchmarks to add to those > already in use (and used in past competitions). A selection of > benchmarks in various categories is used for the competition (according > to rules that are currently being revised). > > If you have benchmarks that you think would be useful to SMT-LIB and > SMT-COMP (and may be made public), please let us know as soon as > possible, even if the material is not quite ready. We will work in > close cooperation with the SMT-LIB maintainers to include such > benchmarks in the SMT-LIB in time to be taken into account for the > competition. The deadline for benchmarks to be used in the 2015 > competition will be announced when the schedule and rules are > finalized. > > PRELIMINARY CALL FOR SOLVERS: > > A submission deadline for solvers will be announced along with the > rules. However, it is useful to the organizing team to know in advance > which and how many solvers may be entering. Thus we request that you > let us know at your earliest convenience if you think you may be > submitting one or more solvers to SMT-COMP'15, particularly if you > think there may be unusual circumstances. > > COMMUNICATION: > > The competition web-site will be at www.smtcomp.org. > > Public email regarding the competition may be sent to > smt...@cs.... > > Announcements will be sent on both smt...@cs... and > sm...@cs.... > > Email to the organizers only may be sent to > smt...@li... > > Sincerely, > The organizing team > > > _______________________________________________ > SMT-LIB mailing list > SM...@cs... > http://www.cs.nyu.edu/mailman/listinfo/smt-lib > |