[Termtools] TPDB -- C-Integer Complexity

[Florian Frohn]

Dear Akihisa,

> please indicate which, if existing benchmarks should be removed.

Since Antonio agreed with the proposed new definition for this category
and (unfortunately) CoFloCo and AProVE are the only participants,
there's no need to remove any examples.

> But is there an (implicit) assumption that only "__VERIFIER_nondet_int"
> can be left undefined? Otherwise, only from declaration "int foo();"
> one cannot assume foo to be deterministic, and the naming shouldn't
> matter.

As far as I can see, the C-Integer Termination category only allows a
single declared but undefined function "__VERIFIER_nondet_int". However,
since we agreed on a different definition for C-Integer Complexity, this
doesn't matter anymore.

Best
Florian


> On 2017/07/31 11:02, Florian Frohn wrote:
>> Dear all,
>>
>> during the preparations for the upcoming TermComp I came across some
>> oddities regarding the category "C-Integer Complexity". First of all,
>> the TPDB contains just 26 examples for this category, but according to
>> the Call for Participation at least 40 examples are required. More
>> importantly, they do not conform to the TermComp definition of C-Integer
>> programs (http://www.termination-portal.org/wiki/C_Integer_Programs).
>> E.g., cBench_bin_search_StepSize2.c uses "nondet" instead of
>> "__VERIFIER_nondet_int" for nondeterminism and it uses division, which
>> is not allowed by the definition.
>>
>> Assuming that we agree on the definition from
>> http://www.termination-portal.org/wiki/C_Integer_Programs (which was
>> discussed when the category "C-Integer Termination" was introduced), I
>> propose to
>>
>> 1. remove all examples that do not conform to the definition,
>> 2. collect new examples, and
>> 3. use the examples from "C-Integer Termination" as fallback (i.e., if
>> less than 40 examples are submitted), even though some of them might be
>> uninteresting for complexity analysis.
>>
>> What do the other participants of this category think?
>>
>> Best
>> Florian
>>
>>
>> PS: Sorry if you received multiple copies of this mail, there were some
>> technical issues.
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lists.lri.fr
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
>