Difference between revisions of "Termination Competition 2014 Registration"

From Termination-Portal.org
Jump to navigationJump to search
Line 53: Line 53:
  
 
* Termination of Programming Languages
 
* Termination of Programming Languages
** C: AProVE, T2
+
** C: AProVE, T2, Ultimate Buchi Automizer
** Java: AProVE
+
** Java: AProVE, Julia
 
** Logic Programming: AProVE
 
** Logic Programming: AProVE
 
** Functional Programming: AProVE
 
** Functional Programming: AProVE

Revision as of 14:30, 14 June 2014

Procedure

Registration (by June 15)

  • get an account on starexec
  • send to the organizer, in email, the name of your solver and the categories that you want to enter

Solver pre-submission (by June 22) and submission (by July 1)

  • upload your solver to starexec. In your solver description on starexec, give: name of solver, name and affiliation of (main) author(s), URL for more detail.
  • send to the organizer, in email, for each of your categories, the pair of solver-id and configuration-id. You can send preliminary id pairs, you can update them until July 1.

Benchmark submission (by July 1)

  • upload benchmarks on starexec (in some subspace of your space)
  • send to organizer, in email, the pathname of this subspace

Note: for the above to work, I need to have read access to your space (your solver, your benchmarks). One method for granting access is described here http://starexec.forumotion.com/t80-how-can-the-space-leader-use-non-public-solvers#189 , I hope there's a less roundabout way. (It seems there is not, so you should: create a subspace of your space, put your solver there, and also copy me to this subspace. I will then link to your solver, from the space where I actually run the experiments/competition.)

Participants

registrations, by (meta-)categories. last updated Sat Jun 14 11:42:05 CEST 2014

(This list to be edited by the competition organizer only. Please send email in case of any errors or omissions.)

  • Termination of Term Rewriting (and Transition Systems)
    • TRS Standard: TTT2, NaTT, AProVE, Wanda
    • SRS Standard: TTT2, NaTT, AProVE
    • TRS Relative: TTT2, AProVE
    • SRS Relative: TTT2, AProVE
    • TRS Standard certified: TTT2, matchbox, AProVE
    • SRS Standard certified: TTT2, matchbox, AProVE
    • TRS Relative certified: TTT2, AProVE
    • SRS Relative certified: TTT2, AProVE
    • TRS Equational: AProVE
    • TRS Conditional: AProVE
    • TRS Context Sensitive: AProVE
    • TRS Innermost: AProVE
    • TRS Outermost: AProVE
    • TRS Innermost certified: AProVE
    • TRS Outermost certified: AProVE
    • Higher-Order rewriting (union beta): Wanda
    • integer transition systems: T2, AProVE, Ctrl
    • Integer TRS: AProVE
  • Complexity Analysis of Term Rewriting
    • Derivational Complexity - Full Rewriting: TCT, CaT
    • Runtime Complexity – Full Rewriting: TCT, CaT
    • Runtime Complexity – Innermost Rewriting: TCT, AProVE
    • Derivational Complexity - Full Rewriting certified: CaT
    • Runtime Complexity – Full Rewriting certified: CaT
    • Runtime Complexity – Innermost Rewriting certified: AProVE
  • Termination of Programming Languages
    • C: AProVE, T2, Ultimate Buchi Automizer
    • Java: AProVE, Julia
    • Logic Programming: AProVE
    • Functional Programming: AProVE
  • Verification of Termination of Term Rewriting
    • TRS Standard: CeTA, Rainbow
    • TRS Relative: CeTA
    • TRS Innermost: CeTA
    • TRS Outermost: CeTA
    • TRS Conditional: CeTA
    • TRS Context-Sensitive: CeTA
    • SRS Standard: CeTA
    • SRS Relative: CeTA
  • Verification of Complexity Analysis of Term Rewriting:
    • Derivational Complexity - Full Rewriting: CeTA
    • Runtime Complexity – Full Rewriting: CeTA

Note on Certified Categories

  • Participants of a certified category need to state which verifier they are targetting (it could be several).
  • Writers of verifiers need to state the syntax and semantics of the certificates that they are accepting (e.g., by publishing their verifier specification and/or implementation, with exact version information)

Note: on starexec, you can choose "ceta-postproc" to get immediate verification (by an earlier CeTA version, and with some extra problems, see https://github.com/jwaldmann/ceta-postproc/issues )

Nothing

(nothing here, except "Four or more headings cause a table of contents to be generated automatically.")