[Termtools] TPDB -- C-Integer Complexity

[Akihisa Yamada]

Dear Florian,

please indicate which, if existing benchmarks should be removed.

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.

Best regards,
Akihisa

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
>

-- 
Akihisa Yamada, Ph.D.
Computational Logic Group, Institute of Computer Science,
University of Innsbruck
http://cl-informatik.uibk.ac.at/~ayamada/