Difference between revisions of "WScT08"

From Termination-Portal.org
Jump to navigationJump to search
 
(10 intermediate revisions by 2 users not shown)
Line 10: Line 10:
 
* local organizer: Johannes Waldmann, HTWK Leipzig
 
* local organizer: Johannes Waldmann, HTWK Leipzig
  
 +
more information:
  
== Registration ==
+
* Minutes (summary)
 
+
** [[WScT08-Minutes-Certification]]
Please register by writing your name here
+
** [[WScT08-Minutes-Competition]]
and the title of the talk you want to give,
+
* [[WScT08-Program]] (includes slides of presentations)
or the topic you want to discuss.
+
* [[WScT08-Registration]]
(Feel free to create wiki pages for your topic, and link from here.)
+
* [[WScT08-Arrangements]]
 
 
* 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.
 

Latest revision as of 13:36, 2 June 2008

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

more information: