we are planning to have CHC-COMP’20 affiliated with HCVS at ETAPS (April 26), and as far as I know the HCVS chairs are reserving a slot for us to present the results.
Here are some questions for everybody in the forum:
(i) deadline for submitting solvers? My current plan would be to put the deadline in the second half of March, and to send out a call within the next 2 weeks;
(ii) should we add any tracks? In 2019 we had LRA, LIA, LIA+array, and LIA-nonlinear. We could consider to add a BV track;
(iii) benchmarks; if you have any benchmarks that can be made public, and are not yet available on github, please put them online. As deadline for this I propose March 15.
(iv) which teams are tentatively interested in participating?
Here is the list of submissions I have received for the test runs:
Spacer: all tracks
PCSat: LIA, LIA-Lin
Ultimate Tree Automizer: all tracks
Ultimate Unihorn Automizer: all tracks
Eldarica-abs: LIA, LIA-lin
ic3ia: LIA-lin, LIA-lin-arrays, LRA-TS
Hors Concours: Eldarica: LIA, LIA-lin, LIA-lin-arrays
We have now put online information about the next edition of the competition, CHC-COMP 2021:
The web page in particular lists the tracks we are planning to evaluate, and tentative deadlines for submitting benchmarks, tools, and competition results.
If you are interested in joining CHC-COMP this year, please contact the organizers within the next couple of days, and provide the following pieces of information:
Or feel free to provide this information in this forum.
Of course we hope for a similar number of participants as in the last years, and maybe a couple of new tools as well; please submit in large numbers and make sure that CHC-COMP stays alive!
Best wishes, Grigory & Philipp
ALLcategory? With non linear clauses and quantifier free clause bodies