[Termtools] Termination Analysis of C Programs in SV-COMP

[Matthias Heizmann]

Dear readers of the termtools list,

I proposed a new category for termination of C programs at the Competition on 
Software Verification and sent the email below to several developers of 
termination tools.

I also want to invite you to participate!

If you also introduce a category for termination of C programs, I support this 
too. In my opinion, an overlap of categories between these two competitions is 
no problem. The different rules, dates and benchmark sets will very likely lead 
to interesting differences in the ranking of the participants.

Best regards,
Matthias

http://swt.informatik.uni-freiburg.de/staff/heizmann





__________________________________________________________________________

Dear developers of termination analysis tools,

in the last weeks several tools competed each other in the 3rd Competition on 
Software Verification. http://sv-comp.sosy-lab.org/2014

In all categories of this competition only safety properties were considered. 
Therefore, I proposed a new category in which termination of C programs is 
analyzed.

This new termination category will already be part in the demonstration 
section of the current(!) SV-COMP.
    http://sv-comp.sosy-lab.org/2014/demo.php

This demonstration section is executed after the "regular" benchmarking phase 
of the SV-COMP. In this demonstration section there are neither awards nor 
trophies, but these categories will hopefully become "regular" categories in 
the next SV-COMP.


I want to invite you to participate!


First, I want to invite you to participate with you tool.
For participation in this demonstration section you do not have to write a 
paper about your competition candidate. Apart from that, the rules of the SV-
COMP apply. 
    http://sv-comp.sosy-lab.org/2014/rules.php
Unfortunately, there is not much time left. I agreed with Dirk Beyer (the 
competition chair) on the following deadlines.
Submission of tools: December 20.
Resubmission possible until December 31.


Furthermore, I want to invite you to contribute benchmarks.
As benchmarks, we use programs written in GNU C. Our tools will have to check 
that the main procedure terminates. The benchmarks have to have a license that 
allows usage and redistribution.
There are already some termination specific examples in the repository
    https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c/termination/
and we will also take examples that were used in other SV-COMP categories.
If you want to contribute, please send me your benchmarks until Tuesday (the 
sooner the better).


Sorry for setting up such an SV-COMP demo category "in the last minute", but I 
think the SV-COMP is a great opportunity to increase the visibility of our 
tools.


Best regards,
Matthias

http://swt.informatik.uni-freiburg.de/staff/heizmann