Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Grigory Fedyukovich
    @grigoryfedyukovich
    Thanks
    YukiSatake
    @YukiSatake
    Nice to meet you, @/all . I'm Yuki Satake who is a student of Unno Hiroshi in University of Tsukuba. We are also interested in participating . Can we still enter our solver for CHC-COMP? (sorry for the late reply)
    Grigory Fedyukovich
    @grigoryfedyukovich
    Hi Yuki, you are welcome! Please try your solver on StarExec as soon as possible and report me about any problems (I recommend to email me directly to grigory.fedyukovich@gmail.com). Also, let me know which categories you are interested in.
    YukiSatake
    @YukiSatake
    @grigoryfedyukovich Thank you so much. I'll send an e-mail to you (from: satake@logic.cs.tsukuba.ac.jp) later. We are interested in LIA track, but if we can remove all bugs of our solver on LRA by the dead line, we would like to enter our solver for the track too.
    Grigory Fedyukovich
    @grigoryfedyukovich
    It is my pleasure to announce that all competition jobs are done, and the winners are identified! The results will be announced in the last session of HCVS today. Please stop by if you are around. We will also have a discussion on the future plans.
    Grigory Fedyukovich
    @grigoryfedyukovich
    For those who didn't make it to Prague, the results of the competition are here: https://chc-comp.github.io/2019/chc-comp19.pdf -- congrats Eldarica, Ultimate Unihorn, and Sally (and Spacer)!
    Let's keep discussing the next steps here.
    alexandernutz
    @alexandernutz
    @grigoryfedyukovich Thanks for doing CHC-comp!
    ... I have one request, too: Could you make this year's benchmark set public? It would be a nice reference set to do benchmarks for CHC-related papers.
    Grigory Fedyukovich
    @grigoryfedyukovich
    Hi Alex, the benchmarks are now publicly available from here: https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=336303. Let me know if you have problems accessing them.
    alexandernutz
    @alexandernutz
    That was fast, thanks! I was able to download them. ("download space" option under "space actions" in each subspace, in case anyone else doesn't know this..)
    Philipp Ruemmer
    @pruemmer

    Hi all,
    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?

    Regards, Philipp

    Hari Govind V K
    @hgvk94
    Hi,
    I am a PhD student under Arie.
    We are interested in submitting Spacer.
    Philipp Ruemmer
    @pruemmer
    Great, thanks!
    Philipp Ruemmer
    @pruemmer
    I have now added the deadlines for this year’s competition on our webpage: https://chc-comp.github.io
    Philipp Ruemmer
    @pruemmer
    Hi all,
    As announced yesterday, ETAPS has been postponed due to the virus situation, it is unclear when it will take place. This also means that HCVS, which is affiliated with ETAPS, will not take place on April 26. We are still discussing the implications for CHC-COMP.
    Best wishes, Philipp
    Hari Govind V K
    @hgvk94
    @pruemmer has there been any decision regarding extending the solver submission deadline ? Would help us a lot if the deadline can be extended by a week.
    Thanks.
    Philipp Ruemmer
    @pruemmer
    Yes, I have decided to extend all deadlines by two weeks, hope this helps! Regards, Philipp
    Hari Govind V K
    @hgvk94
    great. thanks
    Philipp Ruemmer
    @pruemmer
    Hi all,
    in the context of categorizing benchmarks I have also cleaned up the CHC-COMP SMT-LIB dialect a bit. I believe all changes capture points where the previous format definition was too restrictive or imprecise, so should not require modifications in the tools; please speak up if I am wrong here.
    The updated format is here:
    https://chc-comp.github.io/format2020.html
    Changes are:
    (1) allow set-info to specify, e.g., SMT-LIB format version or origin of benchmarks. Those commands can be safely ignored.
    (2) de facto all benchmarks already end with an (exit); this command can be safely ignored as well.
    (3) quantified facts, and cleaned up the case of facts without arguments or quantifiers.
    (4) explicitly allow nullary predicates as well. As I interpret the outcome of the discussion a while ago, all tools are fine with nullary predicates already now.
    Please let me know if any of the modifications might cause trouble!
    Matthias Heizmann
    @Heizmann
    It seems to me that in order to upload (and test) a tool on StarExec, one has to be member of the CHC community. If this is correct, could you add me to this community?
    My StarExec profile is https://www.starexec.org/starexec/secure/details/user.jsp?id=72 (i.e, my user ID is probably 72).
    Philipp Ruemmer
    @pruemmer
    Please apply to become member of CHC!
    Maybe I’m blind, but I don’t see a way to add you directly. To apply, navigate to Spaces - Communities, and then choose the action “join”
    Hari Govind V K
    @hgvk94
    @pruemmer I have uploaded (many) solvers inside my space in starexec.
    1) how do I make them public ?
    2) how do I specify which solver to submit for the competition
    3) can we submit different configurations for different tracks ?
    Matthias Heizmann
    @Heizmann
    @hgvk94 regarding 1) "edit space permissions" (button that is available each of your spaces) / "make public"
    Philipp Ruemmer
    @pruemmer
    Concerning 2) and 3), please just send me a mail!
    Yes, sure, it is possible to use different configurations for the different tracks
    Hari Govind V K
    @hgvk94
    thanks
    Philipp Ruemmer
    @pruemmer

    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
    Sally: LRA-TS
    Eldarica-abs: LIA, LIA-lin
    prophic3: LIA-lin-arrays
    ic3ia: LIA-lin, LIA-lin-arrays, LRA-TS

    Hors Concours: Eldarica: LIA, LIA-lin, LIA-lin-arrays

    Please let me know in case you want to make any corrections to the listed tracks (or I made mistakes)
    I’m doing the test runs now, and will then send you the results, as well as make the benchmarks used in the test runs public
    Philipp Ruemmer
    @pruemmer
    Hi all! I have been discussing the resource limits for the competition with some of the CHC-COMP teams, and would to know the opinion of the other teams as well.
    The main question is whether we should impose a limit on
    (1) wall-clock time, with each job running on a separate CPU with four cores, which might or might not be utilized by a solver.
    (2) CPU time, which means that a solver utilizing multiple cores will eat up its time budget more quickly than a sequential solver.
    Obviously, (1) will lead to parallel solvers getting more computation resources. (2) leads to a (smaller) advantage for sequential solvers, which do not have any overhead due to communication/synchronisation.
    My preference is to go for (2) this year, and to add a dedicated track for parallel solvers next year that applies only a limit on wall-clock time.
    Opinions?
    Philipp Ruemmer
    @pruemmer

    Hi all!

    We have now put online information about the next edition of the competition, CHC-COMP 2021:
    https://chc-comp.github.io/
    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:

    • Name of the solver(s) you are planning to submit
    • Names of the people submitting
    • Tracks you want to join (in particular, concerning the new tracks we are considering for this year)
      [* Further comments or suggestions you might have]

    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

    Arie Gurfinkel
    @agurfinkel
    how come there is no non linear clauses with arrays and arithmetic? That is, modular verification of memory manipulating programs?
    Are all solutions quantifier free? Are clause bodies quantifier free?
    Philipp Ruemmer
    @pruemmer
    I don’t have any statistics on how many non-linear benchmarks with arrays we have; but if you propose to add such a track (LIA-Nonlin-Arrays) we can add it to the list and investigate
    Arie Gurfinkel
    @agurfinkel
    We have gigabytes from seahorn. They are not up on github due to size limits. What about JayHorn?
    Philipp Ruemmer
    @pruemmer
    We do not process solutions, and satisfiability of a set of clauses is defined exactly as in SMT-LIB, in a model-theoretic way. So yes, a set of clauses would be considered sat even if only quantified solutions exist, but you never have to output such a solution in the competition.
    JayHorn does not use the theory of arrays; but if you have SeaHorn benchmarks, maybe you can upload a nice selection of them?
    Arie Gurfinkel
    @agurfinkel
    benchmarks : already asked my coauthors to get current set ready
    Philipp Ruemmer
    @pruemmer
    cool, thanks!
    Arie Gurfinkel
    @agurfinkel
    solutions : would be nice not to mix benchmarks that require quantifiers together with the ones that do not. Otherwise, this distorts the picture since quantifiers make problem (and solution validation) much harder
    Philipp Ruemmer
    @pruemmer
    I just checked again; last year we only used clauses with quantifier-free constraints, and I don’t see a reason to change this for 2021
    I agree, but we do not have an effective way to distinguish those benchmarks
    leo
    @leonardoalt:matrix.org
    [m]
    how about an ALL category? With non linear clauses and quantifier free clause bodies
    Philipp Ruemmer
    @pruemmer
    Which tracks would you want to include in this category?
    There is a danger that few tools would be able to compete in a general track.
    From the competition point of view, I think it is easier to keep the tracks disjoint.
    leo
    @leonardoalt:matrix.org
    [m]
    I'm of course not sure how useful the benchmarks I could contribute would be, but worse case NIA-Arrays-ADT-BV. BV could be stripped out, and I guess I would need to guarantee that the benchmarks are rather LIA
    nonlinear clauses, quantifier free bodies
    but in general I see the value of a "best effort" category, not sure how practical/important that is for the competition
    Grigory Fedyukovich
    @grigoryfedyukovich
    There are new benchmarks for LIA-Lin-Arrays with quantified bodies (and therefore, quantified solutions) from Vienna people (check their paper at FMCAD'20). We've converted them to CHCs.