Difference between revisions of "Termination Competition Steering Committee"

From Termination-Portal.org
Jump to navigationJump to search
 
(30 intermediate revisions by 5 users not shown)
Line 3: Line 3:
 
* a committee, representing all research groups, influences the design and the running of the competition.
 
* a committee, representing all research groups, influences the design and the running of the competition.
  
Currently, the Competition is hosted by the Computational Logic Research Group
+
Currently, the Competition is hosted on StarExec.
of the University of Innsbruck, Austria (Chair: Aart Middeldorp).
 
  
The Competition Committee currently [http://lists.lri.fr/pipermail/termtools/2007-July/000464.html (as of 26 July 2007)]
+
The Competition Committee currently
consists of  
+
consists of
Juergen Giesl,
+
* [https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/florian-frohn/ Florian Frohn], MPI Saarbrücken
Dieter Hofbauer,
+
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
Salvador Lucas,
+
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
Aart Middeldorp,
+
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona
Olivier Pons,
+
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], NII Tokyo
Johannes Waldmann (Chair),
+
 
Hans Zantema.
+
[[Termination_Competition_Steering_Committee_Bylaws]]
 +
 
 +
The steering committee assembled on June 3rd, 2009,
 +
during the Workshop on Termination in Leipzig.
 +
 
 +
[[TC_SC_Meeting_WST09]]
  
 
= Current Votes =
 
= Current Votes =
  
(none)
+
 
  
 
= Proposed Votes =
 
= Proposed Votes =
  
 
The Competition Committee should vote on ...
 
The Competition Committee should vote on ...
(give only some keywords here, link to separate page if necessary. Discussion shall be on termtools.)  
+
(give only some keywords here, link to separate page if necessary. Discussion shall be on termtools.)
 +
 
 +
= Earlier Votes / Issues resolved otherwise =
 +
 
 +
(otherwise = These topics were discussed on the mailing list,
 +
some solution emerged and no-one objected.)
 +
 
 +
 
 +
* (asked 31-Oct-2008) what is the timeout that will be applied
 +
for verification (by coqc) of the termination certificates:
 +
 
 +
<poll>
 +
Timemout for verification
 +
1 minute
 +
3 minutes
 +
10 minutes
 +
</poll>
 +
 
 +
deadline for voting: Monday 3-Nov 12:00 noon CET.
 +
 
 +
See discussion at http://lists.lri.fr/pipermail/termtools/2008-October/000594.html
 +
 
 +
Resolution: 1 minute timeout.
 +
 
 +
* When should the competition start? (asked 30-Oct-2008) http://lists.lri.fr/pipermail/termtools/2008-October/000589.html
 +
Resolution (31-Oct-2008): competition starts
 +
Tuesday 4-Nov-2008 12:00 noon.
 +
The deadline for submission of tool implementations is one hour before the competition starts.
 +
 
  
* What is the status of Coccinelle/Coq? (27-Oct-2008) Current Coccinelle requires coq-8.2-trunk.  
+
* what should be the timeout (for all categories, except complexity): 60 sec or 120 sec ?
** http://lists.lri.fr/pipermail/termtools/2008-October/000556.html
+
Deadline: October 30 , 4 p.m. CET.  
 +
Resolution: three votes for 60 seconds, two votes for 120 seconds.
  
* What is the procedure/deadline for submission of new (public) examples to the TPDB?  (13-Oct-2008)
 
** http://lists.lri.fr/pipermail/termtools/2008-October/000520.html
 
  
* What is the latest possible date to submit a new version of a program? (13-Oct-2008)  
+
* What is the status of Coccinelle/Coq? (27-Oct-2008) Current Coccinelle requires coq-8.2-trunk.  
** http://lists.lri.fr/pipermail/termtools/2008-October/000518.html
+
Resolution (30-Oct-2008): there is a Coccinelle version that works with coq-8.2beta4
** http://lists.lri.fr/pipermail/termtools/2008-October/000562.html
 
  
= Earlier Votes =
+
* What is the procedure/deadline for submission of new (public) examples to the TPDB?  (13-Oct-2008)
 +
Resolution (30-Oct-2008) no bulk submissions before 1-November deadline. But see next item.
  
There was no formal voting. These topics were discussed on the mailing list
+
* What about submission of (late/secret) problems? (29-Oct-2008)
and no-one objected.
+
Resolution (30-Oct-2008): submit until October 31, 10 am CET. see http://lists.lri.fr/pipermail/termtools/2008-October/000585.html
  
 
* Are the categories LP and FP part of the upcoming competition?
 
* Are the categories LP and FP part of the upcoming competition?
Line 44: Line 75:
 
http://lists.lri.fr/pipermail/termtools/2008-October/000519.html
 
http://lists.lri.fr/pipermail/termtools/2008-October/000519.html
  
YES.
+
YES.  
  
 
* Will there be a SRS-certified category?
 
* Will there be a SRS-certified category?
Line 56: Line 87:
  
 
YES
 
YES
 
= Proposed Bylaws =
 
 
 
 
The committee
 
* elects one research group to host the Termination Competition (for some mutually agreeable range of time)
 
* votes on design issues related to the Termination Competition (the Host of the competition tries to implement the design, within reason)
 
* defines Categories (including problem selection, result evaluation) for Competition
 
* reports on results of runs on Categories
 
 
Each research group
 
that is interested in the competition, and has proven this interest
 
by having actually taken part, sends one member into the Committee.
 
 
The Committee elects a Chair that mainly acts as a secretary
 
for voting and reporting.
 
 
The committee can cast votes.
 
Any committer member (mailing list member?) can propose a question for voting.
 
 
The question shall be discussed (for some reasonable time) on the mailing list,
 
where input from all list members is welcome.
 
The wiki pages can be used to record the status of discussion.
 
 
The Chair then formally announces a reasonable time range
 
where committe members may express their vote (e.g. by emailing to the Chair).
 
 
The result of the vote is then announced on the mailing list
 
and recorded on the Wiki page.
 

Latest revision as of 10:30, 21 October 2019

The basic ideas are:

  • one research group hosts (implements, executes) the competition
  • a committee, representing all research groups, influences the design and the running of the competition.

Currently, the Competition is hosted on StarExec.

The Competition Committee currently consists of

Termination_Competition_Steering_Committee_Bylaws

The steering committee assembled on June 3rd, 2009, during the Workshop on Termination in Leipzig.

TC_SC_Meeting_WST09

Current Votes

Proposed Votes

The Competition Committee should vote on ... (give only some keywords here, link to separate page if necessary. Discussion shall be on termtools.)

Earlier Votes / Issues resolved otherwise

(otherwise = These topics were discussed on the mailing list, some solution emerged and no-one objected.)


  • (asked 31-Oct-2008) what is the timeout that will be applied

for verification (by coqc) of the termination certificates:

<poll> Timemout for verification 1 minute 3 minutes 10 minutes </poll>

deadline for voting: Monday 3-Nov 12:00 noon CET.

See discussion at http://lists.lri.fr/pipermail/termtools/2008-October/000594.html

Resolution: 1 minute timeout.

Resolution (31-Oct-2008): competition starts Tuesday 4-Nov-2008 12:00 noon. The deadline for submission of tool implementations is one hour before the competition starts.


  • what should be the timeout (for all categories, except complexity): 60 sec or 120 sec ?

Deadline: October 30 , 4 p.m. CET. Resolution: three votes for 60 seconds, two votes for 120 seconds.


  • What is the status of Coccinelle/Coq? (27-Oct-2008) Current Coccinelle requires coq-8.2-trunk.

Resolution (30-Oct-2008): there is a Coccinelle version that works with coq-8.2beta4

  • What is the procedure/deadline for submission of new (public) examples to the TPDB? (13-Oct-2008)

Resolution (30-Oct-2008) no bulk submissions before 1-November deadline. But see next item.

  • What about submission of (late/secret) problems? (29-Oct-2008)

Resolution (30-Oct-2008): submit until October 31, 10 am CET. see http://lists.lri.fr/pipermail/termtools/2008-October/000585.html

  • Are the categories LP and FP part of the upcoming competition?

(13-Oct-2008) http://lists.lri.fr/pipermail/termtools/2008-October/000519.html

YES.

  • Will there be a SRS-certified category?

(10-Oct-2008)

YES

  • Will certificates be accepted that are verifiable only with Coq-8.2beta4 (and not with 8.1)?

(10-Oct-2008) http://lists.lri.fr/pipermail/termtools/2008-October/000514.html

YES