Termination-Portal.org - User contributions [en]

Termination Competition 2019

2019-03-13T12:05:22Z

Griff: /* Dates */

In 2019, the Termination and Complexity Competition will be affiliated with [https://tacas.info/toolympics.php Toolympics],
with results presented during [https://conf.researchr.org/track/etaps-2019/tacas-2019-papers TACAS 2019], April 7, Prague.

The competition will be run on the [http://www.starexec.org/ StarExec platform],
a few weeks/days before the presentation of results,
at the discretion of the organizer, Akihisa Yamada.

== Dates ==

* Tool and Problem Submission: <s>March 15, 2019</s> March 16, 2019 (AoE)
* Communication of Initial Results: March 22, 2019
* Finalization of Results: March 31, 2019
* Presentation: April 7, 2019

== Competition Categories and Awards ==

The competition contains several categories for termination and complexity from the areas of term rewriting (all categories with HO/FO-TRSs, with- or without strategies) and programming languages (Logic Programming, Haskell, Java, C, integer transition systems, ...)

Proposals for new categories are welcome and will be discussed in [[Termtools|the mailing list]].



A category is only run at the competition if there are at least 2 participants and at least 40 examples
for this category in the underlying termination problem data base.

== Competition Procedure ==

All participants in the same category will be run on
the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.
However, we will try to accept bugfixes if they are sufficiently in advance to the finalization of results.

For those categories devoted to prove only termination or non-termination, the score of a tool is the number of non-contradictory answers minus the given penalization (if any).

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Albert Rubio (chair), UPC Barcelona, Spain
* Christian Sternagel, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany
* Akihisa Yamada, NII, Japan

Organizing Commmittee
* Akihisa Yamada, NII, Japan

== Registration ==

Participants must be registered on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where you plan to enter tools and problems, and then upload your contributions to [http://www.starexec.org StarExec]

Then, please email the competition's organizer (A. Yamada)
indicating which categories you want to participate and the startexec IDs of your account, your tool, and a configuration per category. Participants of the previous competition can just indicate so if they want to participate to the same categories.

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

this refers to StarExec in general, and not to Termination in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* (new in 2019) [https://github.com/StarExec/StarExec/issues issue tracker]
* [https://www.tapatalk.com/groups/starexec/index.php announcements and discussion] ([https://www.tapatalk.com/groups/starexec/app.php/feed combined feed for recent messages])
* (obsolete) [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/AkihisaYamada/starexec-master starexec-master]
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de.

The competition organizers can be reached at akihisayamada<at>nii.ac.jp.

Send new problems for the competition to akihisayamada<at>nii.ac.jp

== Changes with respect to 2018 ==

These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding.
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,
or create a new wiki page and put a link here.

Termination Competition 2018

2018-05-07T18:11:16Z

Griff: /* Registration */

In 2018, the Termination and Complexity Competition  will be affiliated with the [https://www.floc2018.org/ Federated Logic Conference (FLOC 2018)]. The competition will be run on the [http://www.starexec.org/ StarExec platform].

== Dates ==

* Tool Registration: June 8, 2018
* Problem Submission: June 15, 2018
* Updates of Registered Tools: June 29, 2018
* Competition: July 13-14, 2018

== Competition Categories ==

The competition contains several categories for termination and complexity from the areas of term rewriting (all categories with HO/FO-TRSs, with- or without strategies) and programming languages (Logic Programming, Haskell, Java, C, integer transition systems, ...)

== Competition Procedure ==

All participants in the same category will be run on
the existing problems of this category.

There might be modifications of the rules suggested by the organizer and decided by the SC.

The wall-clock timeout will be 300 seconds, and 4 cores will be available (if a tool wants to use concurrent execution).
The tools will be started in their directory and obtain

* the problem file name on the command line,
* and extra info from environment variables, cf. [[Termination Competition 2014 technical details]]

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those problems where a correct answer is (partially) known, any contradictory answer will be penalized by -10 points.


For those categories devoted to prove only termination or non-termination, the score of a tool is the number of non-contradictory answers minus the given penalization (if any).

== Committees ==

Steering Committee
* Jürgen Giesl, RWTH Aachen, Germany
* Albert Rubio (chair), UPC Barcelona, Spain
* Christian Sternagel, Universität Innsbruck, Austria
* Johannes Waldmann, HTWK Leipzig, Germany
* Akihisa Yamada, NII, Japan

Organizing Commmittee
* Johannes Waldmann, HTWK Leipzig, Germany (advisory)
* Akihisa Yamada, NII, Japan

== Registration ==

Participants must register

* on Starexec (so you can upload and test your solver): enter your data at [https://www.starexec.org/starexec/public/registration.jsp StarExecRegistration], indicating the competition categories where they plan to enter tools and problems, and then upload their contributions to [http://www.starexec.org StarExec]

* *and* with the competition's organizer, A. Yamada (so I know what solver/configuration to use). Details will be announced here: [[Termination Competition 2018 Registration]]

Note: if I (A. Yamada) don't know you ("knowing" is roughly symmetrical), then I will ask you to specify: what termination tool you're working on, what competition categories you plan to take part in, your affiliation (in case you're a student, also the name of your advisor/research group leader).

We recommend to register early. After the deadline, access to [http://www.starexec.org StarExec] might be restricted. We need time to prepare the competition, and other competitions may be running in parallel.

It is highly recommended that participants also subscribe to the [http://lists.lri.fr/mailman/listinfo/termtools termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== StarExec Information ==

this refers to StarExec in general, and not to Termination in particular.

* [https://wiki.uiowa.edu/display/stardev/User+Guide user guide]
* [https://www.tapatalk.com/groups/starexec/index.php announcements and discussion] ([https://www.tapatalk.com/groups/starexec/app.php/feed combined feed for recent messages])
* [http://starexec.forumotion.com/ announcements and discussion] (discontinued, but contains some information that is still valid and not available elsewhere)

== Technical Detail ==

The competition will be running on [http://www.starexec.org/ StarExec] - a cross-community solver (tool) execution and benchmark (problem) library service under joint development (since 2012) at the University of Iowa and the University of Miami.

Competition data will be presented via [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] - developed and running at HTWK Leipzig.

Technical details about the execution platform (as of 2014) can be found [http://www.termination-portal.org/wiki/Termination_Competition_2014_technical_details here].

== Contact ==

To contact the steering committee of the termination competition, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de.

The competition organizers can be reached at johannes.waldmann<at>htwk-leipzig.de

Send new problems for the competition to akihisayamada<at>nii.ac.jp

== Changes with respect to 2017 ==

These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding.
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,
or create a new wiki page and put a link here.

Termination Competition Steering Committee

2018-04-27T08:33:38Z

Griff: update the StarExec and new SC

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
* [http://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [https://www.cs.upc.edu/~albert/ Albert Rubio] (Chair), UPC Barcelona
* [http://cl-informatik.uibk.ac.at/users/griff/ Christian Sternagel], U. Innsbruck
* [https://www.imn.htwk-leipzig.de/~waldmann/ Johannes Waldmann], HTWK Leipzig
* [http://group-mmm.org/~ayamada/ Akihisa Yamada], NII Tokyo

[[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.

* 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 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

People:Christian Sternagel

2014-05-30T12:30:41Z

Griff:

{{Person
|firstname=Christian
|middlenames=
|lastname=Sternagel
|titles=
|email=christian.sternagel@uibk.ac.at
|homepage=http://cl-informatik.uibk.ac.at/~griff/
|country=Austria
|university=University of Innsbruck
|department=Computer Science
|role=PhD 
}}

People:Christian Sternagel

2012-02-24T00:50:04Z

Griff:

{{Person
|firstname=Christian
|middlenames=
|lastname=Sternagel
|titles=
|email=c-sterna@jaist.ac.jp
|homepage=http://www.jaist.ac.jp/~c-sterna/
|country=Japan
|university=Japan Advanced Institute of Science and Technology
|department=School of Information Science
|role=Visiting Researcher 
}}

Tools:Cime

2010-04-09T12:46:51Z

Griff: moved Tools:Tool Cime to Tools:Cime: redundant naming

{{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:Tool Cime

2010-04-09T12:46:51Z

Griff: moved Tools:Tool Cime to Tools:Cime: redundant naming

#REDIRECT [[Tools:Cime]]

Tools:IsaFoR

2010-04-09T12:44:02Z

Griff:

{{Tool
|shortname=IsaFoR
|longname=Isabelle Formalization of Rewriting
|homepage=http://cl-informatik.uibk.ac.at/software/ceta/
|country=Austria
|university=LFU Innsbruck
|developers=[[People:Christian Sternagel|Christian Sternagel]] and [[People:René Thiemann|René Thiemann]]
|publication=[[Bibtex:TS09|Certification of Termination Proofs using CeTA]]
}}

News:Proposal - Rename XTC

2010-01-12T08:58:00Z

Griff: Created page with '<!-- Please insert the corresponding information below so that the news page can be generated automatically. Line breaks are allowed! You may use MediaWiki syntax here …'

{{News
|text= See Section 2 of [[Talk:XTC_Format_Specification]].
|date= Jan 12, 2010
}}

Talk:XTC Format Specification

2010-01-12T08:49:35Z

Griff: /* Proposed Change */ new section

== Proposed <predefined> extension ==

''Proposal'': Add a new element <predefined> to <problem> to extend the problem with a (possibly infinite set) of predefined function symbols and rules.

''Rationale'': TRS problems with predefined rules for integers. As there are infinitely many predefined rules ( like 1 + 1 ->
2, 1 + 2 -> 3, ...), those cannot be expressed with the proposed format. Apart from the infinite number of rules, those are normal TRS (with the additional restriction, that occurence of predefined defined symbols on the lhs is forbidden).

=== Syntax ===
Optional element, may occur arbitrary often.

<xs:element name="predefined" type="xs:string" minOccurs="0" maxOccurs="unbounded">
<xs:attribute name="prefix" use="optional" type="xs:string" />
</xs:element>

The value of this element describes the predefined module to include. The optional "prefix" attribute will prefix every function symbol included in the module with the
supplied string. This allows disambiguating when using multiple modules.

Name clashes (not resolved by a prefix) either between different modules or between a module and a TRS are an error.

(SB: Edited the declaration of <xs:element/> so the element can occur 0..* times)
(LN: Added predefined attribute)

=== Modules ===

Other possible modules would be e.g. restricted_integers (like 32-bit integers).

==== unrestricted_integers ====
* integer constants: 0, -1, 1, -2, 2, ...
* integer operations: 0 + 0 -> 0, 0 + 1 -> 1, 2 * 3 -> 6, ...
* comparisons: 0 < 1 -> TRUE, -2 == 3 -> FALSE, ...
* boolean constants: TRUE, FALSE
* boolean operations: not(TRUE) -> FALSE, and(TRUE, FALSE) -> FALSE, ...
* Additional restriction: Predefined defined symbols may not occur on the lhs of rules.

==== "proprietary" modules ====
If a tool wants to define its own modules, it SHOULD use a name like X-$TOOLNAME-$MODULE, e.g. X-APROVE-INTEGERS.

=== Open problems ===

==== Name clashes ====
How to cope with name clashes, if more than one module is used? E.g. both restricted and unrestricted integers would want to declare TRUE, FALSE and boolean operations.

This could be solved by adding an optional prefix to each function symbol, like

<predefined prefix="int.">unrestricted_integers</predefined>

This would give aus int.0, int.-1, int.TRUE, ... Disadvantage of this approach is, that we get incompatible booleans.

(JW: The root of this problem being that booleans seem to be hard-wired into the integer module.
The boolean module should be separate, and the integer module(s) can import it.
Well, there's a huge design space for module systems, disambiguating names etc.)

(LN: This problem cannot be solved without adding a real module system. So I think having built-in booleans in the integer and adding "cast" rules, if it is necessary to interoperate between multiple modules seems like a workable solution)

== Proposed Change ==

As far as I remember, the name XTC was originally planned for the XML format used by certifiers (something like XML Termination Certificate). There is now a different name
for that, namely CPF (see [http://cl-informatik.uibk.ac.at/software/cpf/]). Still, XTC should either be backronymed as Carsten proposed [http://lists.lri.fr/pipermail/termtools/2009-December/000787.html here], or there should be a new name (e.g., XTP for XML Termination Problem).

Bibtex:KSZM09

2009-05-18T14:29:57Z

Griff:

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

<bibtex>
@inproceedings{KSZM09,
author = {Martin Korp and Christian Sternagel and Harald Zankl and Aart Middeldorp},
title = {Tyrolean Termination Tool 2},
booktitle = {Proceedings of the 20th International Conference on Rewriting Techniques and Applications},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
pages = {295--304},
year = 2009,
volume = 5595
}
</bibtex>

Bibtex:KSZM09

2009-05-18T14:29:12Z

Griff:

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

<bibtex>
@inproceedings{KSZM09,
author = {Martin Korp and Christian Sternagel and Harald Zankl and Aart Middeldorp},
title = {Tyrolean Termination Tool 2},
booktitle = {Proceedings of the 20th International Conference on Rewriting Techniques and Applications},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
pages = {295--304},
year = 2009,
volume = 5595,
note = {To appear.}
}
</bibtex>

Bibtex:KSZM09

2009-05-18T14:28:36Z

Griff:

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

<bibtex>
@inproceedings{KSZM09,
author = {Martin Korp and Christian Sternagel and Harald Zankl and Aart Middeldorp},
title = {Tyrolean Termination Tool 2},
booktitle = {Proceedings of the 20th International Conference on Rewriting Techniques and Applications},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {295--304},
year = 2009,
volume = 5595,
note = {To appear.}
}
</bibtex>

Bibtex:KSZM09

2009-05-18T14:24:32Z

Griff:

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

<bibtex>
@inproceedings{KSZM09,
author = {Martin Korp and Christian Sternagel and Harald Zankl and Aart Middeldorp},
title = {Tyrolean Termination Tool 2},
booktitle = {Proceedings RTA '09},
publisher = {Springer},
series = {LNCS},
pages = {295--304},
year = 2009,
volume = 5595,
note = {To appear.}
}
</bibtex>

Bibtex:KSZM09

2009-05-18T14:23:47Z

Griff:

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

<bibtex>
@inproceedings{KSZM09,
author = {Martin Korp and Christian Sternagel and Harald Zankl and Aart Middeldorp},
title = {Tyrolean Termination Tool 2},
booktitle = {Proceedings RTA '09"},
publisher = {Springer},
series = {LNCS},
pages = {295--304},
year = 2009,
volume = 5595,
note = {To appear.}
}
</bibtex>

Bibtex:KSZM09

2009-05-18T14:20:20Z

Griff:

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

<bibtex>
@inproceedings{KSZM09,
author = {Martin Korp and Christian Sternagel and Harald Zankl and Aart Middeldorp},
title = {Tyrolean Termination Tool 2},
booktitle = {Proceedings RTA '09"},
publisher = {Springer},
series = {LNCS},
pages = {295--304},
year = 2009,
note = {To appear.}
}
</bibtex>

Bibtex:KSZM09

2009-05-18T14:19:06Z

Griff: New page:  == BibTex ==  <bibtex> ...

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

<bibtex>
@inproceedings{KSZM09,
author = "M. Korp and C. Sternagel and H. Zankl and A. Middeldorp",
title = "Tyrolean Termination Tool 2",
booktitle = "Proceedings RTA '09",
publisher = "Springer",
series = "LNCS",
pages = "295-304",
year = "2009",
note = "To appear."
}
</bibtex>

Tools:TTT2

2009-05-18T14:09:36Z

Griff:

{{Tool
|shortname= TTT2
|longname= Tyrolean Termination Tool 2
|homepage= http://cl-informatik.uibk.ac.at/software/ttt2/
|country= Austria
|university= LFU Innsbruck
|developers= [[People:Martin Korp|Martin Korp]], [[People:Christian Sternagel|Christian Sternagel]], [[People:Harald Zankl|Harald Zankl]], and [[People:Aart Middeldorp|Aart Middeldorp]]
|publication=[[Bibtex:KSZM09|Tyrolean Termination Tool 2]]
}}

Tools:TTT2

2009-03-20T15:22:42Z

Griff:

{{Tool
|shortname= TTT2
|longname= Tyrolean Termination Tool 2
|homepage= http://colo6-c703.uibk.ac.at/ttt2
|country= Austria
|university= LFU Innsbruck
|developers= [[People:Martin Korp|Martin Korp]], [[People:Christian Sternagel|Christian Sternagel]], [[People:Harald Zankl|Harald Zankl]], and [[People:Aart Middeldorp|Aart Middeldorp]]
}}

Tools:CeTA

2009-03-20T15:22:01Z

Griff: New page: <!-- Please fill in the data so that your tool can be added to some default categories and a simple tool page can be created. You may extend that tool page yourself af...

{{Tool
|shortname=CeTA
|longname=Certified Termination Analysis
|homepage=http://cl-informatik.uibk.ac.at/software/ceta/
|country=Austria
|university=LFU Innsbruck
|developers=[[People:Christian Sternagel|Christian Sternagel]], [[People:René Thiemann|René Thiemann]], and [[People:Harald Zankl|Harald Zankl]]
}}

Termination Competition Platform

2008-11-20T16:47:41Z

Griff: /* Wishlist: Query Interface */

= Note =

There is (will be) a well-defined process of making design decisions w.r.t. the Termination Competition Execution and Presentation Platform (via mailing list, steering committee), and then the Host decides on implementation.

For features that have run through this process, the [http://dev.aspsimon.org/bugzilla/buglist.cgi?bug_file_loc=&bug_file_loc_type=allwordssubstr&bug_id=&bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED termcomp Bugzilla] is the right place for bug reports.

Below here, we just collect some ideas for later consideration.

= Wishlist: Query Interface =

The idea is to provide a web interface for queries over the results data base(s).
We aim for flexibility, but will start with some simple prototype.
Please list here some typical queries that you would want to execute.

* what problems were solved in srs-standard, but not in srs-standard-certified?
* what are the problems that were solved in (insert category here)-2008 but not in 2007 (yes, we plan to import earlier competition results into the data base)?
* what is the problem/tool in (insert category here) with the longest/shortest proof (file size)/execution time?

what might also be helpful: can you name a web site with some configurable query functionality
that you think is especially well-designed and worth learning from?

Christian Sternagel: I would also like to be able to query the problem data base and not only the results data base(s). (J.W.: there is a [http://colo5-c703.uibk.ac.at:8080/termcomp/tpdb/tpsearch.seam query interface for tpdb] already. what features are missing? C.S.: Since it is currently not working, it is merely a placeholder for a query interface.)

Missing features:

* give me all problems from 2007 that are left linear/overlapping/dummy SRSs/... (i.e., properties of problems)
* boolean combination of properties
* wild cards

Termination Competition Platform

2008-11-20T15:01:50Z

Griff: /* Wishlist: Query Interface */

= Note =

There is (will be) a well-defined process of making design decisions w.r.t. the Termination Competition Execution and Presentation Platform (via mailing list, steering committee), and then the Host decides on implementation.

For features that have run through this process, the [http://dev.aspsimon.org/bugzilla/buglist.cgi?bug_file_loc=&bug_file_loc_type=allwordssubstr&bug_id=&bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED termcomp Bugzilla] is the right place for bug reports.

Below here, we just collect some ideas for later consideration.

= Wishlist: Query Interface =

The idea is to provide a web interface for queries over the results data base(s).
We aim for flexibility, but will start with some simple prototype.
Please list here some typical queries that you would want to execute.

* what problems were solved in srs-standard, but not in srs-standard-certified?
* what are the problems that were solved in (insert category here)-2008 but not in 2007 (yes, we plan to import earlier competition results into the data base)?
* what is the problem/tool in (insert category here) with the longest/shortest proof (file size)/execution time?

what might also be helpful: can you name a web site with some configurable query functionality
that you think is especially well-designed and worth learning from?

Christian Sternagel: I would also like to be able to query the problem data base and not only the results data base(s).

* give me all problems from 2007 that are left linear/overlapping/dummy SRSs/...

Termination Competition Platform

2008-11-20T14:58:46Z

Griff: /* Wishlist: Query Interface */

Tools:CaT

2008-11-05T08:06:11Z

Griff:

{{Tool
|shortname=CaT
|longname=Complexity and Termination
|homepage=http://cl-informatik.uibk.ac.at/software/cat/
|country=Austria
|university=University of Innsbruck
|developers=[[People:Martin Korp|Martin Korp]], [[People:Christian Sternagel|Christian Sternagel]] and [[People:Harald Zankl|Harald Zankl]]
}}

MicroTTT

2008-05-21T13:06:17Z

Griff:

MicroTTT is a prototype written in OCaml that generates XML-output as termination proofs using only the dependency pair transformation, estimated dependency graphs, strongly connected components decomposition, and simple projections combined with the subterm criterion. Additionally it is possible to read in such XML-proofs and - using the same methods as for generating a proof - check them for correctness.
* the source code is available [http://cl-informatik.uibk.ac.at/~griff/mttt/mttt.tar.bz2 here]
* the specification of the XML-format [http://cl-informatik.uibk.ac.at/~griff/mttt/rscc.xsd here]
Note that Ruby needs to be installed for compilation of microTTT, since the internal preprocessor of it is written in that language.

MicroTTT

2008-05-21T13:05:47Z

Griff:

MicroTTT is a prototype written in OCaml that generates XML-output as termination proofs using only the dependency pair transformation, estimated dependency graphs, strongly connected components decomposition and simple projections combined with the subterm criterion. Additionally it is possible to read in such XML-proofs and - using the same methods as for generating a proof - check them for correctness.
* the source code is available [http://cl-informatik.uibk.ac.at/~griff/mttt/mttt.tar.bz2 here]
* the specification of the XML-format [http://cl-informatik.uibk.ac.at/~griff/mttt/rscc.xsd here]
Note that Ruby needs to be installed for compilation of microTTT, since the internal preprocessor of it is written in that language.

MicroTTT

2008-05-21T12:58:06Z

Griff:

MicroTTT (<math>\mu</math>TTT)

MicroTTT

2008-05-21T12:57:34Z

Griff: /* \muTTT */

MicroTTT

2008-05-21T12:57:16Z

Griff: New page: =<math>\mu</math>TTT=

=<math>\mu</math>TTT=

WScT08

2008-05-21T12:56:48Z

Griff: /* 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)
** 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: make nodes (more) self-contained
** have system (termination problem) in each node

* DG Approx, SCC analysis
** give topologically sorted list of SCCs
** 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-21T12:55:40Z

Griff: /* 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)
** 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: make nodes (more) self-contained
** have system (termination problem) in each node

* DG Approx, SCC analysis
** give topologically sorted list of SCCs
** 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 [[microTTT] prototype] 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.

Handling DG and SCCs

2008-05-17T14:20:19Z

Griff:

(draft, please extend)
= Dependency Graphs =
how to handle approximations? for every missing edge, indicate why it is not necessary?
= Strongly Connected Components =
Termination Prover computes SCCs and outputs them. Proof assistant does not have to recompute SCCs (which is costly). Prover has to indicate topological ordering on SCCs. Assistant checks that there are no backward edges between components in this ordering.

Handling DG and SCCs

2008-05-17T14:18:19Z

Griff: Handling SCCs moved to Handling DG and SCCs

(Idea, please extend) Termination Prover computes SCCs and outputs them. Proof assistant does not have to recompute SCCs (which is costly). Prover has to indicate topological ordering on SCCs. Assistant checks that there are no backward edges between components in this ordering.

Handling SCCs

2008-05-17T14:18:19Z

Griff: Handling SCCs moved to Handling DG and SCCs

#REDIRECT [[Handling DG and SCCs]]

WScT08

2008-05-17T14:17:42Z

Griff: /* Material */

Handling DG and SCCs

2008-05-17T14:10:59Z

Griff:

WScT08

2008-05-17T14:10:17Z

Griff: /* Material */

WScT08

2008-05-17T14:09:57Z

Griff: /* Material */

Handling DG and SCCs

2008-05-17T14:09:26Z

Griff: New page: (Idea, please extend) Termination Prover computes SCCs and outputs them. Proof assistant does not have to recompute SCCs (which is costly). Prover has to indicate topological ordering on S...

WScT08

2008-05-17T14:06:43Z

Griff: /* Material */

WScT08

2008-05-17T12:37:01Z

Griff: /* Material */

WScT08

2008-05-17T12:36:22Z

Griff: /* Material */

WScT08

2008-05-17T12:34:10Z

Griff: /* Registration */

WScT08

2008-05-17T08:37:30Z

Griff: /* Material */

WScT08

2008-05-17T08:34:20Z

Griff: /* Program */

WScT08

2008-05-15T16:21:04Z

Griff: /* Registration */

WScT08

2008-04-10T10:15:11Z

Griff: /* Registration/Program */

= Workshop on Certified Termination WScT08 =

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/Program ==

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, (Topic: TBA)

== Local Organization ==

Details will be fixed soon. Vote here! (Just mark with "X")

=== Options for location ===

* external conference facility (e.g. http://www.mediencampus-villa-ida.de/ ,rent would be 150 EUR per day), on-site restaurant/catering (additional cost)

* (X) classroom at HTWK (e.g. "Lipsius-Bau" on that map: http://www.htwk-leipzig.de/hochsch/lageplan.pdf , low or no cost) , self-catering (several small restaurants nearby)

=== Options for date/time ===

* workshop start: Saturday
** (X) morning (9 a.m.) or
** noon (1 p.m.)
* Workshop Dinner (Sunday), booking a table at some restaurant
** in the city center
** (X) outskirts (may include walk or tram ride)
* workshop end: Monday
** (X) noon (1 p.m.) or
** afternoon (5 p.m.)

== 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.)

== 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.

People:Christian Sternagel

2008-04-01T08:52:32Z

Griff:

{{Person
|firstname=Christian
|middlenames=
|lastname=Sternagel
|titles=
|email=christian.sternagel@uibk.ac.at
|homepage=http://cl-informatik.uibk.ac.at/~griff/
|country=Austria
|university=Innsbruck
|department=Computer Science
|role=PhD Student 
}}

People:Christian Sternagel

2008-04-01T08:52:02Z

Griff:

{{Person
|firstname=Christian
|middlenames=
|lastname=Sternagel
|titles=
|email=christian.sternagel@uikb.ac.at
|homepage=http://cl-informatik.uibk.ac.at/~griff/
|country=Austria
|university=Innsbruck
|department=Computer Science
|role=PhD Student 
}}

People:Christian Sternagel

2008-04-01T08:51:25Z

Griff: New page: <!-- Please fill in the data so that you can be added to some default categories and a simple user page can be created. You may extend that user page yourself after th...

{{Person
|firstname=Christian
|middlenames=
|lastname=Sternagel
|titles=
|email=christian.sternagel@uikb.ac.at
|homepage=http://cl-informatik.uikb.ac.at/~griff/
|country=Austria
|university=Innsbruck
|department=Computer Science
|role=PhD Student 
}}