WScT08 - Revision history

J.waldmann at 13:36, 2 June 2008

2008-06-02T13:36:16Z

J.waldmann: /* Adjacent event(s) */

2008-06-02T13:34:56Z

Adjacent event(s)

J.waldmann: /* Local Organization */

2008-06-02T13:34:19Z

Local Organization

J.waldmann: /* Registration */

2008-06-02T13:33:42Z

Registration

J.waldmann: /* Program */

2008-06-02T13:33:01Z

Program

J.waldmann: /* Results (Competition) */

2008-06-02T13:31:38Z

Results (Competition)

J.waldmann: /* Results (Certification) */

2008-06-02T13:30:48Z

Results (Certification)

J.waldmann: /* Workshop on Certified Termination WScT08 */

2008-06-02T13:29:44Z

Workshop on Certified Termination WScT08

Urbain: /* Material */

2008-05-28T14:29:45Z

Material

Urbain: /* Material */

2008-05-27T07:24:40Z

Material

@@ Line 12: / Line 12: @@
 more information:
-* [[WScT08-Minutes-Certification]]
+* Minutes (summary)
-* [[WScT08-Minutes-Competition]]
+** [[WScT08-Minutes-Certification]]
-* [[WScT08-Program]]
+** [[WScT08-Minutes-Competition]]
 * [[WScT08-Registration]]
 * [[WScT08-Arrangements]]

← Older revision		Revision as of 13:34, 2 June 2008
Line 17:		Line 17:
	* [[WScT08-Registration]]		* [[WScT08-Registration]]
	* [[WScT08-Arrangements]]		* [[WScT08-Arrangements]]
−
−
−
−
−
−
−	~~== 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.~~

← Older revision		Revision as of 13:34, 2 June 2008
Line 21:		Line 21:


−	~~== 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) ==		== Adjacent event(s) ==

← Older revision		Revision as of 13:33, 2 June 2008
Line 18:		Line 18:
	* [[WScT08-Arrangements]]		* [[WScT08-Arrangements]]

−
−	~~== 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

← Older revision		Revision as of 13:33, 2 June 2008
Line 61:		Line 61:
	* Dieter Hofbauer		* 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]
−
−
−
−
−
−	~~=== Proposed XML Format for Import/Export to the termination database ===~~
−	~~See here: [[TPDB_XML_Format]]~~

	== Local Organization ==		== Local Organization ==

← Older revision		Revision as of 13:31, 2 June 2008
Line 85:		Line 85:


−	~~=== 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 ===		=== Proposed XML Format for Import/Export to the termination database ===

← Older revision		Revision as of 13:30, 2 June 2008
Line 83:		Line 83:
	* 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]		* 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) ===		=== Results (Competition) ===

← Older revision		Revision as of 13:29, 2 June 2008
Line 9:		Line 9:
	* date: May 17 - 19, 2008		* date: May 17 - 19, 2008
	* local organizer: Johannes Waldmann, HTWK Leipzig		* local organizer: Johannes Waldmann, HTWK Leipzig
		+
		+	more information:
		+
		+	* [[WScT08-Minutes-Certification]]
		+	* [[WScT08-Minutes-Competition]]
		+	* [[WScT08-Program]]
		+	* [[WScT08-Registration]]
		+	* [[WScT08-Arrangements]]

@@ Line 72: / Line 72: @@
 * 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/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]