Termination-Portal.org - User contributions [en]

Tools:Cime

2009-05-21T08:30:26Z

Urbain:

{{Tool
|shortname=Cime3
|longname=Cime3
|homepage=http://a3pat.ensiie.fr/pub/index.en.html
|country=France
|university=Cédric (CNAM/ENSIIE) and LRI (Univ. Paris-Sud, CNRS)
|developers=Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain.
|publication=[[Bibtex:Contejean07]]
}}

Tools:A3PAT

2009-05-21T08:28:42Z

Urbain:

{{Tool
|shortname=A3PAT
|longname=Assister Automatiquement les Assistants de Preuve avec des Traces
|homepage=http://a3pat.ensiie.fr/
|country=FR
|university=Cedric, INRIA Sophia-Antipolis, LaBRI, LRI-PCRI
|developers=Y. Bertot, P. Castéran, É. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain
|publication=[[Bibtex:Contejean07]]
}}

Bibtex:Contejean07

2009-05-21T08:22:18Z

Urbain: ref to a3pat added

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>

@InProceedings{contejean07frocos,
author = {Évelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
title = {Certification of automated termination proofs},
booktitle = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
year = 2007,
editor = {Boris Konev and Frank Wolter},
volume = 4720,
pages = {148--162},
series = lnai,
address = {Liverpool,UK},
month = sep,
publisher = sv
}

</bibtex>

Tools:Cime

2009-05-13T10:55:07Z

Urbain:

{{Tool
|shortname=Cime3
|longname=Cime3
|homepage=http://a3pat.ensiie.fr/pub/index.en.html
|country=France
|university=Cédric (CNAM/ENSIIE) and LRI (Univ. Paris-Sud, CNRS)
|developers=Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain.
}}

WScT08

2008-05-28T14:29:45Z

Urbain: /* Material */

= Workshop on Certified Termination WScT08 =

For general information on the workshop topic and history, see [[WScT]].

This will be a working meeting,
with plenty of room for discussion.

* location: Leipzig, Germany
* date: May 17 - 19, 2008
* local organizer: Johannes Waldmann, HTWK Leipzig

== Registration ==

Please register by writing your name here
and the title of the talk you want to give,
or the topic you want to discuss.
(Feel free to create wiki pages for your topic, and link from here.)

* Johannes Waldmann, topics I'd like to see
** the present of Rainbow (give help to people who want to use this, may include some time for actual implementation/hacking)
** future of Rainbow (what has become of the plans we made http://color.loria.fr/workshop.html)

* Christian Sternagel,
** I would like to present ([http://cl-informatik.uibk.ac.at/~griff/WScT08/beamer.pdf Presentation]):
*** summary of what I presented in Nancy last year + progress report
*** short overview of (ongoing) work on formalizing dependency pairs, subterm criterion, and SCC decomposition in Isabelle
** I would like to discuss:
*** how to encode (estimated) dependency graphs and SCCs in Rainbow

* René Thiemann, topics (presented in combination with Simon)
** (fixed) details on upcoming termination competition (TC)
** discussion of TC-details that have to be fixed by the community ([http://cl-informatik.uibk.ac.at/~thiemann/talks/leipzig08RT.pdf Presentation], [http://dev.aspsimon.org/workspace/projectdocs/leipzig-08-handout.pdf Handout containing open questions])

* Simon Bailey, topics:
** the current state of the new implementation of the termination competition.
** The initial project outline can be found [http://dev.aspsimon.org/workspace/projectdocs/outline.pdf here] (This was an informal and internal working document).

* Frederic Blanqui. I can present the current state of Rainbow and CoLoR.

* Adam Koprowski

* Carsten Fuhs

* Raúl Gutiérrez,

* Évelyne Contejean. I and Xavier would like to give a talk on Sunday about the A3Pat approach.

* Xavier Urbain

* Andreas Gebhardt

* Dieter Hofbauer

== Program ==

I think we have two main topics
* A: (future of) certified termination
* B: (certified) termination competition

What's your preference (vote here)
* Saturday: A, Sunday: B
* Saturday: B, Sunday: A
* (X) mixed: Saturday: Introduction, Sunday: Discussion

We should aim for a "results" session on Monday
(write down results of discussion, and open problems).

=== Material ===
* 05/17/08, 09:30 — Christian Sternagel, [http://cl-informatik.uibk.ac.at/~griff/WScT08/beamer.pdf slides]
* 05/17/08, 10:30 — René Thiemann, [http://cl-informatik.uibk.ac.at/~thiemann/talks/leipzig08RT.pdf slides]
* 05/17/08, 11:50 — Simon Bailey, [http://dev.aspsimon.org/workspace/projectdocs/leipzig-presentation.pdf slides]
* 05/17/08, 14:00 — handling DG/SCCs ([[Handling SCCs|Idea]])
* 05/18/08, 09:30 — The A3PAT Approach, [http://a3pat.ensiie.fr/pub/a3patwsct.pdf slides], [http://a3pat.ensiie.fr/pub/a3pat.dtd XML-format of A3PAT]
* 05/19/08, 12:00 — René Thiemann, [http://cl-informatik.uibk.ac.at/~thiemann/xml/aprove.dtd XML-output of AProVE], [http://cl-informatik.uibk.ac.at/~thiemann/xml/aproveToHTML.xsl translator to HTML], [http://cl-informatik.uibk.ac.at/~thiemann/xml/aproveToRainbow.xsl translator to Rainbow], [http://cl-informatik.uibk.ac.at/~thiemann/xml/proof.xml example proof]

=== Results (Certification) ===

* Notation:
** TCG is Termination Certificate Grammar
** Rainbow is the translator from TCG, with several backends (one for Color, one for Isabelle)
** Another format and another translator is CiME from A3PAT
** what's the file extension (.tc, .tcg, .tcf, .xml?)
*** .xtc (xml termination certificate)
** introduce version names/numbers for the format and for the translator(s) (in the .xtc, versioning is by using the proper namespace)

* extend TCG format towards common format:
** make nodes (more) self-contained
** have system (termination problem) in each node

* DG Approx, SCC analysis
** give topologically sorted list of SCCs (A3PAT handles graphs and requests this list)
** have certificate for each missing edge (allow different kinds of certificates)

* want to certify non-termination
** proposal: new top element: disproof
** certify loops (is leaf in proof tree)
*** loop has: start term, sequence of steps, final position (and substitution?)
*** step has: position, rule (and substitution?)
** later: other nodes in non-termination-proof trees?

* extend polynomial and (standard) matrix interpretations to rational domain (new XML node types rational-polynomial-interp and rational-matrix-interp)
** a rational number is an XML node (enum, denom)
** need to provide the delta for the ordering

* apply argument filtering on ordering
** currently, manna-ness has ordering, we want to allow argument-filtering-of-ordering there

* direct checking of TPG trees (no formal verification) might be useful for testing extensions (Christian has a prototype ([[microTTT]]) but not exactly for Rainbow)

* re-use in Color some theorems proved in Coccinelle
** e.g. prover termination by innermost termination (if nonoverlapping)
** modular termination (?)
** perhaps have a general transformation (back and forth)

* plan: generate Isabelle proof from TPG tree

=== Results (Competition) ===

* Unique IDs for problems in database
** Idea: short IDs that can be used in papers
** Different suggested formats (nrs are relative, e.g., 2008-1 and 2009-1 possible):
*** nameOfAuthor-year-nr (problem of uniqueness)
*** abbreviatedNameOfAuthor-year-nr (problem of uniqueness)
*** login-year-nr
*** year-archiveNr-fileNr
*** year-fileNr
*** nr
** Question: Who decides format? Would be nice to have decision soon

* Annotation of termination problems
** Comments can be added by user
** Status at time of submission (open in theory, solved on paper, solved, solved certified, ...)
** Presentation will show above points and computed information (like date of submission, solved by xx tools, ...)

* Submission of many problems
** Zip-files which contain xml-file for adding initial comments, etc.
** Format of xml-file has to be fixed
** Should be same format for adding and for retrieving examples
** To discuss: relation to system-part of XTC-format

* Wishlist for termination competition platform
** Testing should be frequently possible
** Extract challenging problems and letting them run with higher time-limit
** Quotas for experiments? Accessing non-approved examples? Using non-approved tools? Mainly Innsbruck is in charge and makes rules public
** SQL-variant for selection problems and evaluate results, where several properties can be used within queries
** Scoring should be flexible
** Categories as queries (incl. randomSubsetOf(..)) + timeout(s) + scoring
** New category: XML-proofs given, certifiers compete
** Possibility to manually attach proofs for problem (difficult to find/human assisted, or large and put it as challenge for certificating category)
** Open source (Obergurgl 2007 this was stated)
** https

* Discussion whether TRSs should be removed from standard categories which do not satisfy variable condition

* Timeouts for verified competition
** Discussion whether there are separate timeouts on proof-finding and checking, or one global timeout
** Majority was for separate timeouts

=== Proposed XML Format for Import/Export to the termination database ===
See here: [[TPDB_XML_Format]]

== Local Organization ==

=== Date/time ===

session times are provisional

* Saturday 9 -- 12 a.m. and 2 -- 5 p.m., Room Z017
* Sunday 9 -- 12 a.m. and 2 -- 5 p.m., Room Z017
** Workshop Dinner 7 p.m. at
http://www.da-vito-leipzig.de/anfahrt.htm Ristorante da Vito

http://maps.google.com/maps/ms?ie=UTF8&msa=0&ll=51.315016,12.370391&spn=0.006196,0.020041&z=16&msid=101450454289755850579.00044d8175b45ecb94da5

* Monday 9 a.m. -- 1 p.m. , Room Li108

=== Location ===

HTWK, Fachbereich IMN, Gustav-Freytag-Straße 42a, 04275 Leipzig
http://www.htwk-leipzig.de/hochsch/lageplan.pdf
* Z017 in ground floor of Zuse-Bau
* Li108 in first floor of Lipsius-Bau

=== Food ===

* coffee and soda provided at the workshop (small fee)
* lunch Saturday/Sunday: several small restaurants nearby
* lunch Monday: Mensa/Cafeteria HTWK

=== Accomodation ===

You'll find plenty of hotels of all price ranges through the usual
[http://maps.google.de/maps?f=l&hl=de&geocode=&q=hotel&near=Leipzig+Gustav+Freytag+Stra%C3%9Fe&sll=51.315754,12.37009&sspn=0.039108,0.076733&ie=UTF8&ll=51.313823,12.37421&spn=0.019555,0.038366&z=15 search engines]

HTWK is at Karl-Liebknecht-Straße/Richard-Lehmann-Straße.

(note: Hotel Seeblick is not a hotel. And there is no Lake.)

=== Travel info ===

* from Airport Leipzig/Halle to Leipzig Hauptbahnhof (central station, right next to city center): several trains. Takes 15 min, goes every 30 min
* from Hauptbahnhof to HTWK (workshop location): take tram #10 (direction Lößnig) or #11 (direction Markkleeberg Ost), until station "Connewitz Kreuz"
(takes 15 min, goes every 15 min) then walk (5 min).

=== Tourist info ===

places to go:

* cultural/historic/shopping: city center (tram stations Wilhelm-Leuschner-Platz, Augustusplatz)
* entertainment (cafes, restaurants, clubs, bars): Karl-Liebknecht-Straße (tram: Südplatz), Gottschedstraße (tram: Thomaskirche)
* recreation: Clara-Zetkin-Park, Cospudener See

... and there's more (so you'll have to come back for [[WST09]])

== Adjacent event(s) ==

Note that WScT08 is right after
[http://www.orchid.inf.tu-dresden.de/gdp/wata08/ WATA08 Dresden].
(There will even be some termination talks at WATA.)
Travel from Dresden to Leipzig is easy (one hour by train).
Dresden is a major tourist attraction.

WScT08

2008-05-27T07:24:40Z

Urbain: /* Material */

= Workshop on Certified Termination WScT08 =

For general information on the workshop topic and history, see [[WScT]].

This will be a working meeting,
with plenty of room for discussion.

* location: Leipzig, Germany
* date: May 17 - 19, 2008
* local organizer: Johannes Waldmann, HTWK Leipzig

== Registration ==

Please register by writing your name here
and the title of the talk you want to give,
or the topic you want to discuss.
(Feel free to create wiki pages for your topic, and link from here.)

* Johannes Waldmann, topics I'd like to see
** the present of Rainbow (give help to people who want to use this, may include some time for actual implementation/hacking)
** future of Rainbow (what has become of the plans we made http://color.loria.fr/workshop.html)

* Christian Sternagel,
** I would like to present ([http://cl-informatik.uibk.ac.at/~griff/WScT08/beamer.pdf Presentation]):
*** summary of what I presented in Nancy last year + progress report
*** short overview of (ongoing) work on formalizing dependency pairs, subterm criterion, and SCC decomposition in Isabelle
** I would like to discuss:
*** how to encode (estimated) dependency graphs and SCCs in Rainbow

* René Thiemann, topics (presented in combination with Simon)
** (fixed) details on upcoming termination competition (TC)
** discussion of TC-details that have to be fixed by the community ([http://cl-informatik.uibk.ac.at/~thiemann/talks/leipzig08RT.pdf Presentation], [http://dev.aspsimon.org/workspace/projectdocs/leipzig-08-handout.pdf Handout containing open questions])

* Simon Bailey, topics:
** the current state of the new implementation of the termination competition.
** The initial project outline can be found [http://dev.aspsimon.org/workspace/projectdocs/outline.pdf here] (This was an informal and internal working document).

* Frederic Blanqui. I can present the current state of Rainbow and CoLoR.

* Adam Koprowski

* Carsten Fuhs

* Raúl Gutiérrez,

* Évelyne Contejean. I and Xavier would like to give a talk on Sunday about the A3Pat approach.

* Xavier Urbain

* Andreas Gebhardt

* Dieter Hofbauer

== Program ==

I think we have two main topics
* A: (future of) certified termination
* B: (certified) termination competition

What's your preference (vote here)
* Saturday: A, Sunday: B
* Saturday: B, Sunday: A
* (X) mixed: Saturday: Introduction, Sunday: Discussion

We should aim for a "results" session on Monday
(write down results of discussion, and open problems).

=== Material ===
* 05/17/08, 09:30 — Christian Sternagel, [http://cl-informatik.uibk.ac.at/~griff/WScT08/beamer.pdf slides]
* 05/17/08, 10:30 — René Thiemann, [http://cl-informatik.uibk.ac.at/~thiemann/talks/leipzig08RT.pdf slides]
* 05/17/08, 11:50 — Simon Bailey, [http://dev.aspsimon.org/workspace/projectdocs/leipzig-presentation.pdf slides]
* 05/17/08, 14:00 — handling DG/SCCs ([[Handling SCCs|Idea]])
* 05/18/08, 09:30 — The A3PAT Approach, [http://a3pat.ensiie.fr/pub/a3patwsct.pdf slides]
* 05/19/08, 12:00 — René Thiemann, [http://cl-informatik.uibk.ac.at/~thiemann/xml/aprove.dtd XML-output of AProVE], [http://cl-informatik.uibk.ac.at/~thiemann/xml/aproveToHTML.xsl translator to HTML], [http://cl-informatik.uibk.ac.at/~thiemann/xml/aproveToRainbow.xsl translator to Rainbow], [http://cl-informatik.uibk.ac.at/~thiemann/xml/proof.xml example proof]

=== Results (Certification) ===

* Notation:
** TCG is Termination Certificate Grammar
** Rainbow is the translator from TCG, with several backends (one for Color, one for Isabelle)
** Another format and another translator is CiME from A3PAT
** what's the file extension (.tc, .tcg, .tcf, .xml?)
*** .xtc (xml termination certificate)
** introduce version names/numbers for the format and for the translator(s) (in the .xtc, versioning is by using the proper namespace)

* extend TCG format towards common format:
** make nodes (more) self-contained
** have system (termination problem) in each node

* DG Approx, SCC analysis
** give topologically sorted list of SCCs (A3PAT handles graphs and requests this list)
** have certificate for each missing edge (allow different kinds of certificates)

* want to certify non-termination
** proposal: new top element: disproof
** certify loops (is leaf in proof tree)
*** loop has: start term, sequence of steps, final position (and substitution?)
*** step has: position, rule (and substitution?)
** later: other nodes in non-termination-proof trees?

* extend polynomial and (standard) matrix interpretations to rational domain (new XML node types rational-polynomial-interp and rational-matrix-interp)
** a rational number is an XML node (enum, denom)
** need to provide the delta for the ordering

* apply argument filtering on ordering
** currently, manna-ness has ordering, we want to allow argument-filtering-of-ordering there

* direct checking of TPG trees (no formal verification) might be useful for testing extensions (Christian has a prototype ([[microTTT]]) but not exactly for Rainbow)

* re-use in Color some theorems proved in Coccinelle
** e.g. prover termination by innermost termination (if nonoverlapping)
** modular termination (?)
** perhaps have a general transformation (back and forth)

* plan: generate Isabelle proof from TPG tree

=== Results (Competition) ===

* Unique IDs for problems in database
** Idea: short IDs that can be used in papers
** Different suggested formats (nrs are relative, e.g., 2008-1 and 2009-1 possible):
*** nameOfAuthor-year-nr (problem of uniqueness)
*** abbreviatedNameOfAuthor-year-nr (problem of uniqueness)
*** login-year-nr
*** year-archiveNr-fileNr
*** year-fileNr
*** nr
** Question: Who decides format? Would be nice to have decision soon

* Annotation of termination problems
** Comments can be added by user
** Status at time of submission (open in theory, solved on paper, solved, solved certified, ...)
** Presentation will show above points and computed information (like date of submission, solved by xx tools, ...)

* Submission of many problems
** Zip-files which contain xml-file for adding initial comments, etc.
** Format of xml-file has to be fixed
** Should be same format for adding and for retrieving examples
** To discuss: relation to system-part of XTC-format

* Wishlist for termination competition platform
** Testing should be frequently possible
** Extract challenging problems and letting them run with higher time-limit
** Quotas for experiments? Accessing non-approved examples? Using non-approved tools? Mainly Innsbruck is in charge and makes rules public
** SQL-variant for selection problems and evaluate results, where several properties can be used within queries
** Scoring should be flexible
** Categories as queries (incl. randomSubsetOf(..)) + timeout(s) + scoring
** New category: XML-proofs given, certifiers compete
** Possibility to manually attach proofs for problem (difficult to find/human assisted, or large and put it as challenge for certificating category)
** Open source (Obergurgl 2007 this was stated)
** https

* Discussion whether TRSs should be removed from standard categories which do not satisfy variable condition

* Timeouts for verified competition
** Discussion whether there are separate timeouts on proof-finding and checking, or one global timeout
** Majority was for separate timeouts

=== Proposed XML Format for Import/Export to the termination database ===
See here: [[TPDB_XML_Format]]

== Local Organization ==

=== Date/time ===

session times are provisional

* Saturday 9 -- 12 a.m. and 2 -- 5 p.m., Room Z017
* Sunday 9 -- 12 a.m. and 2 -- 5 p.m., Room Z017
** Workshop Dinner 7 p.m. at
http://www.da-vito-leipzig.de/anfahrt.htm Ristorante da Vito

http://maps.google.com/maps/ms?ie=UTF8&msa=0&ll=51.315016,12.370391&spn=0.006196,0.020041&z=16&msid=101450454289755850579.00044d8175b45ecb94da5

* Monday 9 a.m. -- 1 p.m. , Room Li108

=== Location ===

HTWK, Fachbereich IMN, Gustav-Freytag-Straße 42a, 04275 Leipzig
http://www.htwk-leipzig.de/hochsch/lageplan.pdf
* Z017 in ground floor of Zuse-Bau
* Li108 in first floor of Lipsius-Bau

=== Food ===

* coffee and soda provided at the workshop (small fee)
* lunch Saturday/Sunday: several small restaurants nearby
* lunch Monday: Mensa/Cafeteria HTWK

=== Accomodation ===

You'll find plenty of hotels of all price ranges through the usual
[http://maps.google.de/maps?f=l&hl=de&geocode=&q=hotel&near=Leipzig+Gustav+Freytag+Stra%C3%9Fe&sll=51.315754,12.37009&sspn=0.039108,0.076733&ie=UTF8&ll=51.313823,12.37421&spn=0.019555,0.038366&z=15 search engines]

HTWK is at Karl-Liebknecht-Straße/Richard-Lehmann-Straße.

(note: Hotel Seeblick is not a hotel. And there is no Lake.)

=== Travel info ===

* from Airport Leipzig/Halle to Leipzig Hauptbahnhof (central station, right next to city center): several trains. Takes 15 min, goes every 30 min
* from Hauptbahnhof to HTWK (workshop location): take tram #10 (direction Lößnig) or #11 (direction Markkleeberg Ost), until station "Connewitz Kreuz"
(takes 15 min, goes every 15 min) then walk (5 min).

=== Tourist info ===

places to go:

* cultural/historic/shopping: city center (tram stations Wilhelm-Leuschner-Platz, Augustusplatz)
* entertainment (cafes, restaurants, clubs, bars): Karl-Liebknecht-Straße (tram: Südplatz), Gottschedstraße (tram: Thomaskirche)
* recreation: Clara-Zetkin-Park, Cospudener See

... and there's more (so you'll have to come back for [[WST09]])

== Adjacent event(s) ==

Note that WScT08 is right after
[http://www.orchid.inf.tu-dresden.de/gdp/wata08/ WATA08 Dresden].
(There will even be some termination talks at WATA.)
Travel from Dresden to Leipzig is easy (one hour by train).
Dresden is a major tourist attraction.

WScT08

2008-05-26T12:26:15Z

Urbain: /* Results (Certification) */

= Workshop on Certified Termination WScT08 =

For general information on the workshop topic and history, see [[WScT]].

This will be a working meeting,
with plenty of room for discussion.

* location: Leipzig, Germany
* date: May 17 - 19, 2008
* local organizer: Johannes Waldmann, HTWK Leipzig

== Registration ==

Please register by writing your name here
and the title of the talk you want to give,
or the topic you want to discuss.
(Feel free to create wiki pages for your topic, and link from here.)

* Johannes Waldmann, topics I'd like to see
** the present of Rainbow (give help to people who want to use this, may include some time for actual implementation/hacking)
** future of Rainbow (what has become of the plans we made http://color.loria.fr/workshop.html)

* Christian Sternagel,
** I would like to present ([http://cl-informatik.uibk.ac.at/~griff/WScT08/beamer.pdf Presentation]):
*** summary of what I presented in Nancy last year + progress report
*** short overview of (ongoing) work on formalizing dependency pairs, subterm criterion, and SCC decomposition in Isabelle
** I would like to discuss:
*** how to encode (estimated) dependency graphs and SCCs in Rainbow

* René Thiemann, topics (presented in combination with Simon)
** (fixed) details on upcoming termination competition (TC)
** discussion of TC-details that have to be fixed by the community ([http://cl-informatik.uibk.ac.at/~thiemann/talks/leipzig08RT.pdf Presentation], [http://dev.aspsimon.org/workspace/projectdocs/leipzig-08-handout.pdf Handout containing open questions])

* Simon Bailey, topics:
** the current state of the new implementation of the termination competition.
** The initial project outline can be found [http://dev.aspsimon.org/workspace/projectdocs/outline.pdf here] (This was an informal and internal working document).

* Frederic Blanqui. I can present the current state of Rainbow and CoLoR.

* Adam Koprowski

* Carsten Fuhs

* Raúl Gutiérrez,

* Évelyne Contejean. I and Xavier would like to give a talk on Sunday about the A3Pat approach.

* Xavier Urbain

* Andreas Gebhardt

* Dieter Hofbauer

== Program ==

I think we have two main topics
* A: (future of) certified termination
* B: (certified) termination competition

What's your preference (vote here)
* Saturday: A, Sunday: B
* Saturday: B, Sunday: A
* (X) mixed: Saturday: Introduction, Sunday: Discussion

We should aim for a "results" session on Monday
(write down results of discussion, and open problems).

=== Material ===
* 05/17/08, 09:30 — Christian Sternagel, [http://cl-informatik.uibk.ac.at/~griff/WScT08/beamer.pdf slides]
* 05/17/08, 10:30 — René Thiemann, [http://cl-informatik.uibk.ac.at/~thiemann/talks/leipzig08RT.pdf slides]
* 05/17/08, 11:50 — Simon Bailey, [http://dev.aspsimon.org/workspace/projectdocs/leipzig-presentation.pdf slides]
* 05/17/08, 14:00 — handling DG/SCCs ([[Handling SCCs|Idea]])
* 05/19/08, 12:00 — René Thiemann, [http://cl-informatik.uibk.ac.at/~thiemann/xml/aprove.dtd XML-output of AProVE], [http://cl-informatik.uibk.ac.at/~thiemann/xml/aproveToHTML.xsl translator to HTML], [http://cl-informatik.uibk.ac.at/~thiemann/xml/aproveToRainbow.xsl translator to Rainbow], [http://cl-informatik.uibk.ac.at/~thiemann/xml/proof.xml example proof]

=== Results (Certification) ===

* Notation:
** TCG is Termination Certificate Grammar
** Rainbow is the translator from TCG, with several backends (one for Color, one for Isabelle)
** Another format and another translator is CiME from A3PAT
** what's the file extension (.tc, .tcg, .tcf, .xml?)
*** .xtc (xml termination certificate)
** introduce version names/numbers for the format and for the translator(s) (in the .xtc, versioning is by using the proper namespace)

* extend TCG format towards common format:
** make nodes (more) self-contained
** have system (termination problem) in each node

* DG Approx, SCC analysis
** give topologically sorted list of SCCs (A3PAT handles graphs and requests this list)
** have certificate for each missing edge (allow different kinds of certificates)

* want to certify non-termination
** proposal: new top element: disproof
** certify loops (is leaf in proof tree)
*** loop has: start term, sequence of steps, final position (and substitution?)
*** step has: position, rule (and substitution?)
** later: other nodes in non-termination-proof trees?

* extend polynomial and (standard) matrix interpretations to rational domain (new XML node types rational-polynomial-interp and rational-matrix-interp)
** a rational number is an XML node (enum, denom)
** need to provide the delta for the ordering

* apply argument filtering on ordering
** currently, manna-ness has ordering, we want to allow argument-filtering-of-ordering there

* direct checking of TPG trees (no formal verification) might be useful for testing extensions (Christian has a prototype ([[microTTT]]) but not exactly for Rainbow)

* re-use in Color some theorems proved in Coccinelle
** e.g. prover termination by innermost termination (if nonoverlapping)
** modular termination (?)
** perhaps have a general transformation (back and forth)

* plan: generate Isabelle proof from TPG tree

=== Results (Competition) ===

* Unique IDs for problems in database
** Idea: short IDs that can be used in papers
** Different suggested formats (nrs are relative, e.g., 2008-1 and 2009-1 possible):
*** nameOfAuthor-year-nr (problem of uniqueness)
*** abbreviatedNameOfAuthor-year-nr (problem of uniqueness)
*** login-year-nr
*** year-archiveNr-fileNr
*** year-fileNr
*** nr
** Question: Who decides format? Would be nice to have decision soon

* Annotation of termination problems
** Comments can be added by user
** Status at time of submission (open in theory, solved on paper, solved, solved certified, ...)
** Presentation will show above points and computed information (like date of submission, solved by xx tools, ...)

* Submission of many problems
** Zip-files which contain xml-file for adding initial comments, etc.
** Format of xml-file has to be fixed
** Should be same format for adding and for retrieving examples
** To discuss: relation to system-part of XTC-format

* Wishlist for termination competition platform
** Testing should be frequently possible
** Extract challenging problems and letting them run with higher time-limit
** Quotas for experiments? Accessing non-approved examples? Using non-approved tools? Mainly Innsbruck is in charge and makes rules public
** SQL-variant for selection problems and evaluate results, where several properties can be used within queries
** Scoring should be flexible
** Categories as queries (incl. randomSubsetOf(..)) + timeout(s) + scoring
** New category: XML-proofs given, certifiers compete
** Possibility to manually attach proofs for problem (difficult to find/human assisted, or large and put it as challenge for certificating category)
** Open source (Obergurgl 2007 this was stated)
** https

* Discussion whether TRSs should be removed from standard categories which do not satisfy variable condition

* Timeouts for verified competition
** Discussion whether there are separate timeouts on proof-finding and checking, or one global timeout
** Majority was for separate timeouts

=== Proposed XML Format for Import/Export to the termination database ===
See here: [[TPDB_XML_Format]]

== Local Organization ==

=== Date/time ===

session times are provisional

* Saturday 9 -- 12 a.m. and 2 -- 5 p.m., Room Z017
* Sunday 9 -- 12 a.m. and 2 -- 5 p.m., Room Z017
** Workshop Dinner 7 p.m. at
http://www.da-vito-leipzig.de/anfahrt.htm Ristorante da Vito

http://maps.google.com/maps/ms?ie=UTF8&msa=0&ll=51.315016,12.370391&spn=0.006196,0.020041&z=16&msid=101450454289755850579.00044d8175b45ecb94da5

* Monday 9 a.m. -- 1 p.m. , Room Li108

=== Location ===

HTWK, Fachbereich IMN, Gustav-Freytag-Straße 42a, 04275 Leipzig
http://www.htwk-leipzig.de/hochsch/lageplan.pdf
* Z017 in ground floor of Zuse-Bau
* Li108 in first floor of Lipsius-Bau

=== Food ===

* coffee and soda provided at the workshop (small fee)
* lunch Saturday/Sunday: several small restaurants nearby
* lunch Monday: Mensa/Cafeteria HTWK

=== Accomodation ===

You'll find plenty of hotels of all price ranges through the usual
[http://maps.google.de/maps?f=l&hl=de&geocode=&q=hotel&near=Leipzig+Gustav+Freytag+Stra%C3%9Fe&sll=51.315754,12.37009&sspn=0.039108,0.076733&ie=UTF8&ll=51.313823,12.37421&spn=0.019555,0.038366&z=15 search engines]

HTWK is at Karl-Liebknecht-Straße/Richard-Lehmann-Straße.

(note: Hotel Seeblick is not a hotel. And there is no Lake.)

=== Travel info ===

* from Airport Leipzig/Halle to Leipzig Hauptbahnhof (central station, right next to city center): several trains. Takes 15 min, goes every 30 min
* from Hauptbahnhof to HTWK (workshop location): take tram #10 (direction Lößnig) or #11 (direction Markkleeberg Ost), until station "Connewitz Kreuz"
(takes 15 min, goes every 15 min) then walk (5 min).

=== Tourist info ===

places to go:

* cultural/historic/shopping: city center (tram stations Wilhelm-Leuschner-Platz, Augustusplatz)
* entertainment (cafes, restaurants, clubs, bars): Karl-Liebknecht-Straße (tram: Südplatz), Gottschedstraße (tram: Thomaskirche)
* recreation: Clara-Zetkin-Park, Cospudener See

... and there's more (so you'll have to come back for [[WST09]])

== Adjacent event(s) ==

Note that WScT08 is right after
[http://www.orchid.inf.tu-dresden.de/gdp/wata08/ WATA08 Dresden].
(There will even be some termination talks at WATA.)
Travel from Dresden to Leipzig is easy (one hour by train).
Dresden is a major tourist attraction.