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
the following solvers have registered for CHC-COMP 2021:
Golem: LIA-Lin, LRA-TS, LRA-TS-parallel
Spacer: LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, LRA-TS, LRA-TS-parallel, ADT-NonLin
PCSat: LIA-Lin, LIA-NonLin, ADT-NonLin
Ultimate TreeAutomizer: LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, LRA-TS, LRA-TS-parallel
Ultimate UniHorn: LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, LRA-TS, LRA-TS-parallel
Eldarica (HC): LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, ADT-NonLin
We removed the ADT-Lin track, since we could not put together a useful set of benchmarks for this track.
The deadline for sending us the final version of the solvers is March 18.
You can find example benchmarks in the CHC space on StarExec, https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=442129
Regards, Grigory & Philipp