|
|
| (7 intermediate revisions by the same user 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/18/08, 09:30 — The A3PAT Approach, [http://a3pat.ensiie.fr/pub/a3patwsct.pdf slides], [http://a3pat.ensiie.fr/pub/a3pat.dtd XML-format of A3PAT] | |
| − | * 05/19/08, 12:00 — René Thiemann, [http://cl-informatik.uibk.ac.at/~thiemann/xml/aprove.dtd XML-output of AProVE], [http://cl-informatik.uibk.ac.at/~thiemann/xml/aproveToHTML.xsl translator to HTML], [http://cl-informatik.uibk.ac.at/~thiemann/xml/aproveToRainbow.xsl translator to Rainbow], [http://cl-informatik.uibk.ac.at/~thiemann/xml/proof.xml example proof]
| |
| − | | |
| − | === Results (Certification) ===
| |
| − | | |
| − | * Notation:
| |
| − | ** TCG is Termination Certificate Grammar
| |
| − | ** Rainbow is the translator from TCG, with several backends (one for Color, one for Isabelle)
| |
| − | ** Another format and another translator is CiME from A3PAT
| |
| − | ** what's the file extension (.tc, .tcg, .tcf, .xml?)
| |
| − | *** .xtc (xml termination certificate)
| |
| − | ** introduce version names/numbers for the format and for the translator(s) (in the .xtc, versioning is by using the proper namespace)
| |
| − | | |
| − | | |
| − | * extend TCG format towards common format:
| |
| − | ** make nodes (more) self-contained
| |
| − | ** have system (termination problem) in each node
| |
| − | | |
| − | * DG Approx, SCC analysis
| |
| − | ** give topologically sorted list of SCCs (A3PAT handles graphs and requests this list)
| |
| − | ** have certificate for each missing edge (allow different kinds of certificates) | |
| − | | |
| − | * want to certify non-termination
| |
| − | ** proposal: new top element: disproof
| |
| − | ** certify loops (is leaf in proof tree)
| |
| − | *** loop has: start term, sequence of steps, final position (and substitution?)
| |
| − | *** step has: position, rule (and substitution?)
| |
| − | ** later: other nodes in non-termination-proof trees?
| |
| − | | |
| − | * extend polynomial and (standard) matrix interpretations to rational domain (new XML node types rational-polynomial-interp and rational-matrix-interp)
| |
| − | ** a rational number is an XML node (enum, denom)
| |
| − | ** need to provide the delta for the ordering
| |
| − | | |
| − | * apply argument filtering on ordering
| |
| − | ** currently, manna-ness has ordering, we want to allow argument-filtering-of-ordering there
| |
| − | | |
| − | * direct checking of TPG trees (no formal verification) might be useful for testing extensions (Christian has a prototype ([[microTTT]]) but not exactly for Rainbow)
| |
| − | | |
| − | * re-use in Color some theorems proved in Coccinelle
| |
| − | ** e.g. prover termination by innermost termination (if nonoverlapping)
| |
| − | ** modular termination (?)
| |
| − | ** perhaps have a general transformation (back and forth)
| |
| − | | |
| − | * plan: generate Isabelle proof from TPG tree
| |
| − | | |
| − | === Results (Competition) ===
| |
| − | | |
| − | * Unique IDs for problems in database
| |
| − | ** Idea: short IDs that can be used in papers
| |
| − | ** Different suggested formats (nrs are relative, e.g., 2008-1 and 2009-1 possible):
| |
| − | *** nameOfAuthor-year-nr (problem of uniqueness)
| |
| − | *** abbreviatedNameOfAuthor-year-nr (problem of uniqueness)
| |
| − | *** login-year-nr
| |
| − | *** year-archiveNr-fileNr
| |
| − | *** year-fileNr
| |
| − | *** nr
| |
| − | ** Question: Who decides format? Would be nice to have decision soon
| |
| − | | |
| − | * Annotation of termination problems
| |
| − | ** Comments can be added by user
| |
| − | ** Status at time of submission (open in theory, solved on paper, solved, solved certified, ...)
| |
| − | ** Presentation will show above points and computed information (like date of submission, solved by xx tools, ...)
| |
| − |
| |
| − | * Submission of many problems
| |
| − | ** Zip-files which contain xml-file for adding initial comments, etc.
| |
| − | ** Format of xml-file has to be fixed
| |
| − | ** Should be same format for adding and for retrieving examples
| |
| − | ** To discuss: relation to system-part of XTC-format
| |
| − | | |
| − | * Wishlist for termination competition platform
| |
| − | ** Testing should be frequently possible
| |
| − | ** Extract challenging problems and letting them run with higher time-limit
| |
| − | ** Quotas for experiments? Accessing non-approved examples? Using non-approved tools? Mainly Innsbruck is in charge and makes rules public
| |
| − | ** SQL-variant for selection problems and evaluate results, where several properties can be used within queries
| |
| − | ** Scoring should be flexible
| |
| − | ** Categories as queries (incl. randomSubsetOf(..)) + timeout(s) + scoring
| |
| − | ** New category: XML-proofs given, certifiers compete
| |
| − | ** Possibility to manually attach proofs for problem (difficult to find/human assisted, or large and put it as challenge for certificating category)
| |
| − | ** Open source (Obergurgl 2007 this was stated)
| |
| − | ** https
| |
| − | | |
| − | | |
| − | * Discussion whether TRSs should be removed from standard categories which do not satisfy variable condition
| |
| − | | |
| − | * Timeouts for verified competition
| |
| − | ** Discussion whether there are separate timeouts on proof-finding and checking, or one global timeout
| |
| − | ** Majority was for separate timeouts
| |
| − | | |
| − | === Proposed XML Format for Import/Export to the termination database ===
| |
| − | See here: [[TPDB_XML_Format]]
| |
| − | | |
| − | == Local Organization ==
| |
| − | | |
| − | === Date/time ===
| |
| − | | |
| − | session times are provisional
| |
| − | | |
| − | * Saturday 9 -- 12 a.m. and 2 -- 5 p.m., Room Z017
| |
| − | * Sunday 9 -- 12 a.m. and 2 -- 5 p.m., Room Z017
| |
| − | ** Workshop Dinner 7 p.m. at
| |
| − | http://www.da-vito-leipzig.de/anfahrt.htm Ristorante da Vito
| |
| − | | |
| − | http://maps.google.com/maps/ms?ie=UTF8&msa=0&ll=51.315016,12.370391&spn=0.006196,0.020041&z=16&msid=101450454289755850579.00044d8175b45ecb94da5
| |
| − | | |
| − | | |
| − | * Monday 9 a.m. -- 1 p.m. , Room Li108
| |
| − | | |
| − | === Location ===
| |
| − | | |
| − | HTWK, Fachbereich IMN, Gustav-Freytag-Straße 42a, 04275 Leipzig
| |
| − | http://www.htwk-leipzig.de/hochsch/lageplan.pdf
| |
| − | * Z017 in ground floor of Zuse-Bau
| |
| − | * Li108 in first floor of Lipsius-Bau
| |
| − | | |
| − | === Food ===
| |
| − | | |
| − | * coffee and soda provided at the workshop (small fee)
| |
| − | * lunch Saturday/Sunday: several small restaurants nearby
| |
| − | * lunch Monday: Mensa/Cafeteria HTWK
| |
| − | | |
| − | === Accomodation ===
| |
| − | | |
| − | You'll find plenty of hotels of all price ranges through the usual
| |
| − | [http://maps.google.de/maps?f=l&hl=de&geocode=&q=hotel&near=Leipzig+Gustav+Freytag+Stra%C3%9Fe&sll=51.315754,12.37009&sspn=0.039108,0.076733&ie=UTF8&ll=51.313823,12.37421&spn=0.019555,0.038366&z=15 search engines]
| |
| − | | |
| − | HTWK is at Karl-Liebknecht-Straße/Richard-Lehmann-Straße.
| |
| − | | |
| − | (note: Hotel Seeblick is not a hotel. And there is no Lake.)
| |
| − | | |
| − | === Travel info ===
| |
| − | | |
| − | * from Airport Leipzig/Halle to Leipzig Hauptbahnhof (central station, right next to city center): several trains. Takes 15 min, goes every 30 min
| |
| − | * from Hauptbahnhof to HTWK (workshop location): take tram #10 (direction Lößnig) or #11 (direction Markkleeberg Ost), until station "Connewitz Kreuz"
| |
| − | (takes 15 min, goes every 15 min) then walk (5 min).
| |
| − | | |
| − | === Tourist info ===
| |
| − | | |
| − | places to go:
| |
| − | | |
| − | * cultural/historic/shopping: city center (tram stations Wilhelm-Leuschner-Platz, Augustusplatz) | |
| − | * entertainment (cafes, restaurants, clubs, bars): Karl-Liebknecht-Straße (tram: Südplatz), Gottschedstraße (tram: Thomaskirche)
| |
| − | * recreation: Clara-Zetkin-Park, Cospudener See
| |
| − | | |
| − | ... and there's more (so you'll have to come back for [[WST09]])
| |
| − | | |
| − | == Adjacent event(s) ==
| |
| − | | |
| − | Note that WScT08 is right after
| |
| − | [http://www.orchid.inf.tu-dresden.de/gdp/wata08/ WATA08 Dresden].
| |
| − | (There will even be some termination talks at WATA.)
| |
| − | Travel from Dresden to Leipzig is easy (one hour by train).
| |
| − | Dresden is a major tourist attraction.
| |
