TC

Information about TC

Published on October 9, 2007

Author: Heather

Source: authorstream.com

Content

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 organizer Running 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 1 TRS 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: aabc, bbac, ccab

Related presentations


Other presentations created by Heather

nanotechnology presentation
13. 10. 2007
0 views

nanotechnology presentation

MMLA group ppt 11 28 05
08. 10. 2008
0 views

MMLA group ppt 11 28 05

Sadiq
08. 05. 2008
0 views

Sadiq

Mun101806
08. 05. 2008
0 views

Mun101806

ch09r
08. 05. 2008
0 views

ch09r

louise baur
08. 05. 2008
0 views

louise baur

Obesity
07. 05. 2008
0 views

Obesity

radev
07. 05. 2008
0 views

radev

pp pres sptconfrday
06. 05. 2008
0 views

pp pres sptconfrday

pp pres sptconfrday
06. 05. 2008
0 views

pp pres sptconfrday

Communication skills notes
26. 11. 2007
0 views

Communication skills notes

L12 Superconductivity
12. 10. 2007
0 views

L12 Superconductivity

Development of behavior
11. 10. 2007
0 views

Development of behavior

Silver Sword Review
19. 10. 2007
0 views

Silver Sword Review

Notes Russia
27. 09. 2007
0 views

Notes Russia

thesis
30. 09. 2007
0 views

thesis

spiritual warefare combined2
01. 10. 2007
0 views

spiritual warefare combined2

ASAPJan06 Presentation Millonig
03. 10. 2007
0 views

ASAPJan06 Presentation Millonig

symp04 pp liming e
10. 10. 2007
0 views

symp04 pp liming e

China India Web FINAL POST
10. 10. 2007
0 views

China India Web FINAL POST

reptile powerpoint
12. 10. 2007
0 views

reptile powerpoint

Heatsub
12. 10. 2007
0 views

Heatsub

Notes Europe
15. 10. 2007
0 views

Notes Europe

Funding Biomedical Research
16. 10. 2007
0 views

Funding Biomedical Research

NEW chpt 4
17. 10. 2007
0 views

NEW chpt 4

ATUG power point presentation
17. 10. 2007
0 views

ATUG power point presentation

ANT3141 20 Peru
19. 10. 2007
0 views

ANT3141 20 Peru

Implication du Personnel
24. 10. 2007
0 views

Implication du Personnel

lecture 45
02. 10. 2007
0 views

lecture 45

McK CIT 05 PC2A
15. 10. 2007
0 views

McK CIT 05 PC2A

chapter2 notes
15. 10. 2007
0 views

chapter2 notes

brun
28. 10. 2007
0 views

brun

Branson HIV and Privacy 2
29. 10. 2007
0 views

Branson HIV and Privacy 2

Oracle OTC
05. 11. 2007
0 views

Oracle OTC

Darwinismo
06. 11. 2007
0 views

Darwinismo

WRITING unit 3 summaries 95
18. 10. 2007
0 views

WRITING unit 3 summaries 95

lecture28
16. 11. 2007
0 views

lecture28

VirologyReview2005
19. 11. 2007
0 views

VirologyReview2005

Martha
20. 11. 2007
0 views

Martha

gender selection
21. 11. 2007
0 views

gender selection

ulrich 120203
30. 10. 2007
0 views

ulrich 120203

LPP600 ch5 rev
06. 11. 2007
0 views

LPP600 ch5 rev

dance
23. 11. 2007
0 views

dance

rutas de putaendo
24. 10. 2007
0 views

rutas de putaendo

Insomnia 2
28. 11. 2007
0 views

Insomnia 2

marktoberdorf
30. 10. 2007
0 views

marktoberdorf

PacketSwitching1
30. 12. 2007
0 views

PacketSwitching1

Manshadi impact
03. 01. 2008
0 views

Manshadi impact

Ionizing Radiation 2
04. 01. 2008
0 views

Ionizing Radiation 2

egov ma
23. 10. 2007
0 views

egov ma

chap15a
05. 01. 2008
0 views

chap15a

lecture hazard individual choice
04. 10. 2007
0 views

lecture hazard individual choice

Spanish presentation
22. 10. 2007
0 views

Spanish presentation

presentazione estetismo
01. 10. 2007
0 views

presentazione estetismo

BVS Panama
22. 10. 2007
0 views

BVS Panama

Hollywood
25. 10. 2007
0 views

Hollywood

astro12Summer11
13. 11. 2007
0 views

astro12Summer11

ryud
09. 10. 2007
0 views

ryud

MetaphorsWeLiveBy
24. 10. 2007
0 views

MetaphorsWeLiveBy

AMMA briefing
06. 11. 2007
0 views

AMMA briefing

west africa down
03. 01. 2008
0 views

west africa down

zhping PHD
04. 10. 2007
0 views

zhping PHD

Ch02
15. 10. 2007
0 views

Ch02

02Coelho Review
16. 10. 2007
0 views

02Coelho Review

RUSSIA transition
26. 10. 2007
0 views

RUSSIA transition

39124236 GEOMORPHOLOGY RIVERS
19. 10. 2007
0 views

39124236 GEOMORPHOLOGY RIVERS

AFlood2005
03. 01. 2008
0 views

AFlood2005

26 Beautiful One liners 09 12 06
07. 10. 2007
0 views

26 Beautiful One liners 09 12 06

milia v10
21. 02. 2008
0 views

milia v10

BRT LA Metro
29. 10. 2007
0 views

BRT LA Metro

18531
24. 02. 2008
0 views

18531

gulf war 2 desert storm
26. 02. 2008
0 views

gulf war 2 desert storm

NDBs MSC SA Mondi
27. 02. 2008
0 views

NDBs MSC SA Mondi

t2nd edn
16. 03. 2008
0 views

t2nd edn

AsiaPacificUpdate
25. 03. 2008
0 views

AsiaPacificUpdate

Lecture23 SmallSats
15. 11. 2007
0 views

Lecture23 SmallSats

BU NSF06 kannan
31. 10. 2007
0 views

BU NSF06 kannan

Macro Chapter 4
10. 04. 2008
0 views

Macro Chapter 4

mini supercells jmm final
03. 10. 2007
0 views

mini supercells jmm final

SPS CM Seminar
14. 04. 2008
0 views

SPS CM Seminar

lecture13 Online Games
22. 04. 2008
0 views

lecture13 Online Games

IDN Gold WebEx BSE
22. 04. 2008
0 views

IDN Gold WebEx BSE

NIV oncall
01. 05. 2008
0 views

NIV oncall

history stuff
14. 12. 2007
0 views

history stuff

abadinsky08 ppt ch03
07. 01. 2008
0 views

abadinsky08 ppt ch03

The BioArtificial Liver2
02. 05. 2008
0 views

The BioArtificial Liver2

Katrina RRC
02. 05. 2008
0 views

Katrina RRC

angusallyouneed tcm4 123635
02. 10. 2007
0 views

angusallyouneed tcm4 123635

ladeau
21. 10. 2007
0 views

ladeau

Presentation10
09. 04. 2008
0 views

Presentation10

Food web of the Arctic
10. 10. 2007
0 views

Food web of the Arctic

Barbara 01
26. 09. 2007
0 views

Barbara 01

Befmod Dog Pony Big
17. 04. 2008
0 views

Befmod Dog Pony Big

EHaro Presentacion Casablanca
24. 10. 2007
0 views

EHaro Presentacion Casablanca

Turner Powerpoint
31. 12. 2007
0 views

Turner Powerpoint

Feb27
07. 10. 2007
0 views

Feb27

2005 Kobe
09. 10. 2007
0 views

2005 Kobe

liberal jun2000 tapia
15. 10. 2007
0 views

liberal jun2000 tapia

hiv and smoking
29. 10. 2007
0 views

hiv and smoking

157 4s1 10p35 voloshin
26. 10. 2007
0 views

157 4s1 10p35 voloshin

cicognani
11. 10. 2007
0 views

cicognani

paper55
29. 10. 2007
0 views

paper55

Mission and Vision
07. 01. 2008
0 views

Mission and Vision

2004 07 01 rochoa
15. 11. 2007
0 views

2004 07 01 rochoa

Seva activities at Bridgewater
10. 12. 2007
0 views

Seva activities at Bridgewater

African lag
05. 10. 2007
0 views

African lag

8 Barbra Morgante RFI
15. 10. 2007
0 views

8 Barbra Morgante RFI

Vajente GWDAW11 StatusOfVirgo
01. 12. 2007
0 views

Vajente GWDAW11 StatusOfVirgo

papineni
15. 10. 2007
0 views

papineni

housemtg 20040907
16. 10. 2007
0 views

housemtg 20040907

ClevelandStateF2005
02. 11. 2007
0 views

ClevelandStateF2005

IDC prezentace LinuxWorld
24. 10. 2007
0 views

IDC prezentace LinuxWorld

stassun
01. 01. 2008
0 views

stassun

Models User Guide
05. 10. 2007
0 views

Models User Guide

Suite Sensation General
07. 12. 2007
0 views

Suite Sensation General

Suchman Virology 2005
16. 10. 2007
0 views

Suchman Virology 2005

jd graz
18. 03. 2008
0 views

jd graz

veronarda
03. 10. 2007
0 views

veronarda

RHIC spin talk
15. 11. 2007
0 views

RHIC spin talk

Nian Cai Liu presentation
15. 10. 2007
0 views

Nian Cai Liu presentation