Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    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.
    Philipp Ruemmer
    @pruemmer
    ok, it would be great to upload all available benchmarks on github, we can then see which tracks make sense!
    for NIA-Array-ADT-BV, I suspect few solvers will qualify ;-)
    Philipp Ruemmer
    @pruemmer

    Hi all,

    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
    RegInv: 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

    Philipp Ruemmer
    @pruemmer
    Correction: the name of “RegInv” changed to “RInGen”
    leo
    @leonardoalt:matrix.org
    [m]
    Hi there!
    I started uploading some benchmarks from my tool that folks might find useful:
    https://github.com/leonardoalt/chc_benchmarks_solidity
    How about an Industry track for next CHC comp? 😬
    That would mean: every SMT theory is available, nonlinear clauses too.
    Currently only Spacer and Eldarica can solve these benchmarks, but maybe the competition would incentivize other solvers to get there?
    Grigory Fedyukovich
    @grigoryfedyukovich
    Thanks, Leo! So it's a combination of theories, I guess? Can you list them here?
    IMHO, we need at least three solvers to register for a track. And Spacer next year will not compete since Hari is one of the organizers.
    leo
    @leonardoalt:matrix.org
    [m]
    NIA, Arrays, ADTs (only tuples, non-recursive), potentially BV but that I can remove, nonlinear clauses
    Grigory Fedyukovich
    @grigoryfedyukovich
    If you unfold tuples and get rid of BV, that would be just NIA+Arrays, so maybe that will make them more approachable by other solvers. Also, what kind of NIA? I could not find *, div, or mod there.
    3 replies
    Hari Govind V K
    @hgvk94
    I am hoping that Eldarica can participate instead of Spacer.
    leo
    @leonardoalt:matrix.org
    [m]
    Regarding tuples, that's true. That would make my encoding a lot more complicated though, not sure I have the current bandwidth to make that change in my code. Maybe eventually we'll have a pre-processing tool that does that pass, since that might be useful for other applications as well besides mine.
    Yea that's true, the actual code only has linear division and mod, and after some equality propagation the horn code too.
    Ah wait, you're talking about abi, you're right.
    It's a single benchmark but it's a lot more meaningful though. The application it comes from currently holds 37 billion usd, whereas my thousands of unit tests hold nothing haha
    1 reply
    leo
    @leonardoalt:matrix.org
    [m]
    How so?
    (it's public code and that info is also public, if that's what you're referring to)
    1 reply
    leo
    @leonardoalt:matrix.org
    [m]
    I'll see what I can do about unfolding the tuples, would make sense in general.
    1 reply
    If you use Matrix/Element you can!
    (Gitter channels are also Matrix channels now after it was bought)
    2 replies
    leo
    @leonardoalt:matrix.org
    [m]
    Yea true, I remember Gitter had that but always found it kinda buggy.
    1 reply
    You can use both, one for emojis one for threads.
    Yurii Kostyukov
    @Columpio
    Hello, everyone. We are now going to make SAT/UNSAT validator for CHC-COMP with our students. As we have seen, there are some tools for that already on https://github.com/chc-comp/chc-tools
    However, there is no chc_is_refute actually and chc_is_model does not work even for examples/ from repository (it gives Z3 parsing error)
    Could anyone elaborate on that? What's the status of chc_is_refute and chc_is_model?
    1 reply