logging in or signing up TC Heather Download Post to : URL : Related Presentations : Share Add to Flag Embed Email Send to Blogs and Networks Add to Channel Uploaded from authorPOINTLite Insert YouTube videos in PowerPont slides with aS Desktop Copy embed code: (To copy code, click on the text box) Embed: URL: Thumbnail: WordPress Embed Customize Embed The presentation is successfully added In Your Favorites. Views: 44 Category: Entertainment License: All Rights Reserved Like it (0) Dislike it (0) Added: October 09, 2007 This Presentation is Public Favorites: 0 Presentation Description No description available. Comments Posting comment... Premium member Presentation Transcript Termination competition 2005 http://www.lri.fr/~marche/termination-competition/2005/: Termination competition 2005 http://www.lri.fr/~marche/termination-competition/2005/ Claude Marché Hans Zantema Université Paris-Sud TU Eindhoven France The Netherlands Objective:: Objective: Compare various tools for proving termination of programs, TRSs,…. by running them on an extensive set TPDB (termination problem data base) of termination problems Stimulate research in this area, shifting emphasis towards automation Provide a standard to valuate (new) termination techniques History:: History: WST 2003, Valencia, Albert Rubio, development of TPDB WST 2004, Aachen, Claude Marché, actual competition executed fully automatically the week before April 2005, reported at RTA, Nara Categories:: Categories: (logic) programs: not this year TRS: term rewriting Termination (773) Innermost termination (65) Termination modulo AC (54) Context-sensitive (not this year) Conditional rewriting (not this year) Relative termination (34) SRS: string rewriting Termination (153) Relative termination (13)How did we manage?: How did we manage? Full schedule and rules of the game announced in advance Open submission of new problems for TPDB until few weeks before competition This TPDB was publicly available for testing and tuning the tools Just before competition: participants submitted Final versions of the tools Secret problems, up to 5 per participant per category In this way participants also being organizer had no advantage of being organizerRunning the competition: Running the competition Secret problems added to TPDB All tools apply on all problems in the corresponding TPDB categories, all on the same machine Results are: YES, followed by text of proof (sketch) NO, followed by text of proof (sketch) DON’T KNOW, or time-out (1 minute for every problem) All results are reported on-line, including generated proof text, and statistics about scores and running time Total running time: several days All this machinery was developed by Claude Marché The participants: The participants AProVE (Aachen: Jürgen Giesl, Peter Schneider-Kamp, René Thiemann, ….) CiME (Paris: Claude Marché, ….) Jambox (Leipzig: Jörg Endrullis) Matchbox (Leipzig: Johannes Waldmann) TEPARLA (Eindhoven: Jeroen van der Wulp) TORPA (Eindhoven: Hans Zantema) TPA (Eindhoven: Adam Koprowski) TTT (Tsukuba, Innsbrück: Aart Middeldorp, Nao Hirokawa)SRS results: SRS results Total number 153 13 YES time NO relative AProVE 114 3.4 4 CiME 37 2.4 - Jambox 102 2.1 9 Matchbox 66 1.4 9 TEPARLA 74 3.7 1 11 TORPA 126 0.04 5 12 TPA 65 3.5 - 10 TTT 60 0.4 1TRS results: TRS results standard innermost AC relative Total number 773 65 54 34 YES time NO YES No YES YES AProVE 576 1.7 94 63 1 51 CiME 311 1.0 - 42 Matchbox 165 3.1 80 TEPARLA 347 1.2 15 15 TPA 407 1.4 - 23 TTT 509 0.46 1 50 -Conclusions: Conclusions Big improvements compared to 2004 Best tool in TRS category: AProVE Best tool in SRS category: TORPA Tools giving proofs for which all other tools failed: AProVE, CiME, Jambox, TEPARLA, TORPA, TPA Executables of all tools available Impact: big participants remain colleagues rather than competitors non-participating tools not taken serious any more Still unsolved: aabc, bbac, ccab You do not have the permission to view this presentation. In order to view it, please contact the author of the presentation.
TC Heather Download Post to : URL : Related Presentations : Share Add to Flag Embed Email Send to Blogs and Networks Add to Channel Uploaded from authorPOINTLite Insert YouTube videos in PowerPont slides with aS Desktop Copy embed code: (To copy code, click on the text box) Embed: URL: Thumbnail: WordPress Embed Customize Embed The presentation is successfully added In Your Favorites. Views: 44 Category: Entertainment License: All Rights Reserved Like it (0) Dislike it (0) Added: October 09, 2007 This Presentation is Public Favorites: 0 Presentation Description No description available. Comments Posting comment... Premium member Presentation Transcript Termination competition 2005 http://www.lri.fr/~marche/termination-competition/2005/: Termination competition 2005 http://www.lri.fr/~marche/termination-competition/2005/ Claude Marché Hans Zantema Université Paris-Sud TU Eindhoven France The Netherlands Objective:: Objective: Compare various tools for proving termination of programs, TRSs,…. by running them on an extensive set TPDB (termination problem data base) of termination problems Stimulate research in this area, shifting emphasis towards automation Provide a standard to valuate (new) termination techniques History:: History: WST 2003, Valencia, Albert Rubio, development of TPDB WST 2004, Aachen, Claude Marché, actual competition executed fully automatically the week before April 2005, reported at RTA, Nara Categories:: Categories: (logic) programs: not this year TRS: term rewriting Termination (773) Innermost termination (65) Termination modulo AC (54) Context-sensitive (not this year) Conditional rewriting (not this year) Relative termination (34) SRS: string rewriting Termination (153) Relative termination (13)How did we manage?: How did we manage? Full schedule and rules of the game announced in advance Open submission of new problems for TPDB until few weeks before competition This TPDB was publicly available for testing and tuning the tools Just before competition: participants submitted Final versions of the tools Secret problems, up to 5 per participant per category In this way participants also being organizer had no advantage of being organizerRunning the competition: Running the competition Secret problems added to TPDB All tools apply on all problems in the corresponding TPDB categories, all on the same machine Results are: YES, followed by text of proof (sketch) NO, followed by text of proof (sketch) DON’T KNOW, or time-out (1 minute for every problem) All results are reported on-line, including generated proof text, and statistics about scores and running time Total running time: several days All this machinery was developed by Claude Marché The participants: The participants AProVE (Aachen: Jürgen Giesl, Peter Schneider-Kamp, René Thiemann, ….) CiME (Paris: Claude Marché, ….) Jambox (Leipzig: Jörg Endrullis) Matchbox (Leipzig: Johannes Waldmann) TEPARLA (Eindhoven: Jeroen van der Wulp) TORPA (Eindhoven: Hans Zantema) TPA (Eindhoven: Adam Koprowski) TTT (Tsukuba, Innsbrück: Aart Middeldorp, Nao Hirokawa)SRS results: SRS results Total number 153 13 YES time NO relative AProVE 114 3.4 4 CiME 37 2.4 - Jambox 102 2.1 9 Matchbox 66 1.4 9 TEPARLA 74 3.7 1 11 TORPA 126 0.04 5 12 TPA 65 3.5 - 10 TTT 60 0.4 1TRS results: TRS results standard innermost AC relative Total number 773 65 54 34 YES time NO YES No YES YES AProVE 576 1.7 94 63 1 51 CiME 311 1.0 - 42 Matchbox 165 3.1 80 TEPARLA 347 1.2 15 15 TPA 407 1.4 - 23 TTT 509 0.46 1 50 -Conclusions: Conclusions Big improvements compared to 2004 Best tool in TRS category: AProVE Best tool in SRS category: TORPA Tools giving proofs for which all other tools failed: AProVE, CiME, Jambox, TEPARLA, TORPA, TPA Executables of all tools available Impact: big participants remain colleagues rather than competitors non-participating tools not taken serious any more Still unsolved: aabc, bbac, ccab