Difference between revisions of "Termination Competition Steering Committee"

From Termination-Portal.org
Jump to navigationJump to search
 
(37 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 on StarExec.
  
−
Currently, the Competition is hosted by the Computational Logic Research Group
+
The Competition Committee currently
−
of the University of Innsbruck, Austria (Chair: Aart Middeldorp).
+
consists of
 +
* [https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/florian-frohn/ Florian Frohn], MPI Saarbrücken
 +
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
 +
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
 +
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona
 +
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], NII Tokyo
  
−
The Competition Committee currently consists of .. and the Chair is Johannes Waldmann (HTWK Leipzig, Germany).
+
[[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.
  
−
= Earlier Votes =
+
* 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.
  
−
(none)
 
  
 +
* 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.
  
−
= Proposed Bylaws =
 
  
 +
* 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.
  
−
The committee
+
* What about submission of (late/secret) problems? (29-Oct-2008)
−
* elects one research group to host the Termination Competition (for some mutually agreeable range of time)
+
Resolution (30-Oct-2008): submit until October 31, 10 am CET. see http://lists.lri.fr/pipermail/termtools/2008-October/000585.html
−
* 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
+
* Are the categories LP and FP part of the upcoming competition?
−
that is interested in the competition, and has proven this interest
+
(13-Oct-2008)
−
by having actually taken part, sends one member into the Committee.
+
http://lists.lri.fr/pipermail/termtools/2008-October/000519.html
  
−
The Committee elects a Chair that mainly acts as a secretary
+
YES.  
−
for voting and reporting.
 
  
−
The committee can cast votes.
+
* Will there be a SRS-certified category?
−
Any committer member (mailing list member?) can propose a question for voting.
+
(10-Oct-2008)
  
−
The question shall be discussed (for some reasonable time) on the mailing list,
+
YES
−
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
+
* Will certificates be accepted that are verifiable only with Coq-8.2beta4 (and not with 8.1)?
−
where committe members may express their vote (e.g. by emailing to the Chair).
+
(10-Oct-2008)
 +
http://lists.lri.fr/pipermail/termtools/2008-October/000514.html
  
−
The result of the vote is then announced on the mailing list
+
YES
−
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

Retrieved from "http://termination-portal.org/mediawiki/index.php?title=Termination_Competition_Steering_Committee&oldid=1833"