Termination-Portal.org - User contributions [en]

WST09

2009-06-04T11:43:42Z

Binabik:

The 10th Workshop on Termination will be held in 2009 in Leipzig, Germany.

== general information ==

See the [http://www.imn.htwk-leipzig.de/wst09/ official workshop page]

== wishlist ==

(add suggestions here)

== slides/presentations ==
termexec/tpdb query interface: http://dev.aspsimon.org/workspace/projectdocs/leipzig-wst09.pdf

Termination Competition Platform

2009-04-01T15:29:26Z

Binabik:

= 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 are the problems that generate a coq timeout for some tool?
* what is the average size of the (xml|coq) files generated by a given tool?
* what are the (problems|results) that are (solved|certified) by all the tools in some set of tools?

* here is a [http://color.loria.fr/comp.html result presentation for Color in certified categories] that Frederic built "by hand" (?) The query interface should automatically produce such or and similar charts.

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
* give results statistics for parts of a category, e.g., only selected subdirectories

= Execution Component =
The termination competition platform will be extended by a component allowing users to create custom experiments comparing different tools on a custom selection of termination problems. the document linked below outlines the proposed functionality this component will offer.

http://dev.aspsimon.org/workspace/projectdocs/termexec.pdf

Termination Competition 2008

2009-04-01T12:58:39Z

Binabik:

From 2008 onwards, the competition will be ongoing:
submission of new problems and provers is possible anytime via...

* [http://termcomp.uibk.ac.at/termcomp/ Termination Competition Execution Platform] ([http://lists.lri.fr/pipermail/termtools/2008-October/000511.html how to submit])

Still, there will be certain deadlines where
all data is collected and a report is produced. Upcoming deadlines are:

* (for sure) 1 November 2008
* (tentative) somewhere in May 2009 (so that a report can be presented at the Termination Workshop in June 2009)

The [Termination Problem Data Base 5.0] [http://dev.aspsimon.org/projects/termcomp/downloads/]
is used for the competition 2008.

While implementation of the execution platform is handled by the Host of the competition,
here is a separate page (a wishlist) for design issues: [[Termination_Competition_Platform]].

Talk:XTC Format Specification

2009-02-26T08:00:29Z

Binabik: /* Syntax */

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

The value of this element describes the predefined module to include.

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

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

XTC Format Specification

2009-02-13T13:08:31Z

Binabik:

= Schema =
For now see http://dev.aspsimon.org/xtc.xsd

= XML Structure =
The XML structure has the following main blocks:

* <trs>: this block contains all the information pertinent to the TRS itself. A more detailed description is below.
* <strategy>: this corresponds to the (STRATEGY ) block in the TPDB format.
* <startterm>: this is an extension for complexity analysis
* <status>: this is a meta-information block which contains information relating to the known termination status of a given problem.
*<metainformation>: more meta-information pertaining to the author of a problem, can also contain free-form comments.

Both <status> and <metainformation> will be stored in the database, but stripped from input files for the purposes of running the competition.

The <trs> block is structured as follows:

* <rules>: this block contains all the rules of a TRS, relative rules are separated into a separate child <relrules>; both these blocks can contain multiple <rule> children, consisting of a <lhs>, <rhs> and optional <conditions> block.
* <signature>: this block contains the list of function symbols with their signatures (name, arity, theory and context-sensitive replacement-map).
* <comment>: a free-form comment field about this TRS itself.
*<conditiontype>: for conditional TRS, this block is used to select the type of condition to be applied.

The full structure can be seen in the XML Schema file linked above.

= XSLT Transformation =
The stylesheet can be found here: http://dev.aspsimon.org/workspace/projectdownloads/xtc2tpdb.xsl. More information to follow.

XTC Format Specification

2009-02-13T12:16:29Z

Binabik:

= Schema =
For now see http://dev.aspsimon.org/xtc.xsd

= XSLT Transformation =
The stylesheet can be found here: http://dev.aspsimon.org/workspace/projectdownloads/xtc2tpdb.xsl. More information to follow.

XTC Format Specification

2009-02-13T12:10:18Z

Binabik: New page: For now see http://dev.aspsimon.org/xtc.xsd

For now see http://dev.aspsimon.org/xtc.xsd

WST09

2008-05-19T09:53:24Z

Binabik:

The 10th Workshop on Termination will be held in 2009 in Leipzig, Germany.

* local organization: Alfons Geser and Johannes Waldmann, HTWK Leipzig
* venue (to be confirmed): http://www.mml-leipzig.de/ueber-das-mml/mediencampus/
* general tourist information: http://www.leipzig.de/

What are your preferences for the date of the workshop? Vote here:

* around June 2 - 7 (week after Whitsunday = Pfingsten)
** Probably June 4-7 will be best.
* around July 6 - 11

Do you know of any conflicting or adjacent conferences? (Please list dates here.)
* RTA09 (RDP09) June 28 - July 3 in Brasilia

What length do we want for the workshop? E.g. three full days,
starting with an informal reception on the day before.

=== Certified Termination ===
Should certified termination be part of the program? If so, should it be contained on one day or spread over the days? Discuss!

WST09

2008-05-19T09:52:23Z

Binabik:

WScT08

2008-05-19T09:12:18Z

Binabik: /* Local Organization */

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

=== 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 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
** Structured query-language for selections and runs, where several properties can be used within queries
** Possibility to manually attach (large) proofs; perhaps new category: certification of these proofs

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

TPDB XML Format

2008-05-19T09:09:12Z

Binabik: New page: == A proposal for an XML grammar for termination problems == Still needs to be formalised and completed. <pre><code> <tp version="1.0"> <meta> <author/> <date/> <originalcomment/>...

== A proposal for an XML grammar for termination problems ==

Still needs to be formalised and completed.

<pre><code>
<tp version="1.0">
<meta>
<author/>
<date/>
<originalcomment/>
</meta>
<termination>
<theory><theorydecl>Multiple</theorydecl></theory>
<strategy>
<INNERMOST/> |
<OUTERMOST/> |
<CONTEXTSENSITIVE>
<contextsensitivestuff/>
</CONTEXTSENSITIVE>
|<NONE/>
</strategy>
<conditional type="ltr|join"/>
<type>TRS|SRS</type>
<status>TERMINATES|DOESNTERMINATE|DUNNO</status>
</termination>
<rules>
<rule nonstrict="true|false" top="yes|no|maybe"> 
<lhs>
<term>
<function> 
<variable name="a|..."/>
</function>
</term>
<variable name="a|..."/>
</lhs>
<rhs>$term</rhs>
</rule>
<conditionalrule>
<conditions>
<rule/> 
</conditions>
<rule/>
</conditionalrule>
</rules>

<signature>


</signature>
</tp>
</code></pre>

WScT08

2008-05-17T12:06:18Z

Binabik: /* Material */

WScT08

2008-05-17T12:05:09Z

Binabik: /* Material */

WScT08

2008-05-17T08:26:35Z

Binabik:

WScT08

2008-05-17T08:23:58Z

Binabik:

WScT08

2008-05-17T08:23:32Z

Binabik:

WScT08

2008-05-17T08:23:12Z

Binabik:

WScT08

2008-05-14T11:13:21Z

Binabik: /* Registration */