Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Robots at the Edge of the Cloud Read chapter Read first chapter

2016 | OriginalPaper | Chapter

TcT: Tyrolean Complexity Tool

Authors : Martin Avanzini, Georg Moser, Michael Schaper

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In this paper we present https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49674-9_24/419290_1_En_24_IEq1_HTML.gif v3.0, the latest version of our fully automated complexity analyser. https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49674-9_24/419290_1_En_24_IEq2_HTML.gif implements our framework for automated complexity analysis and focuses on extensibility and automation. https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49674-9_24/419290_1_En_24_IEq3_HTML.gif is open with respect to the input problem under investigation and the resource metric in question. It is the most powerful tool in the realm of automated complexity analysis of term rewrite systems. Moreover it provides an expressive problem-independent strategy language that facilitates proof search. We give insights about design choices, the implementation of the framework and report different case studies where we have applied https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49674-9_24/419290_1_En_24_IEq4_HTML.gif successfully.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems
next chapter Integrated Environment for Diagnosing Verification Errors
Footnotes
1
See for example the results of https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49674-9_24/419290_1_En_24_IEq14_HTML.gif at this year’s TERMCOMP, available from http://​termination-portal.​org/​wiki/​Termination_​Competition_​2015/​.
 
Literature
1.
Albert, E., Arenas, P., Genaim, S., Puebla, G., Román-Díez, G.: Conditional termination of loops over heap-allocated data. SCP 92, 2–24 (2014)
2.
3.
4.
Avanzini, M., Dal Lago, U., Moser, G.: Analysing the complexity of functional programs: higher-order meets first-order. In: Proceeding of the 20th ICFP, pp. 152–164. ACM (2015)
5.
Avanzini, M., Moser, G.: Tyrolean complexity tool: features and usage. In: Proceeding of the 24th RTA, LIPIcs, vol. 21, pp. 71–80 (2013)
6.
Avanzini, M., Moser, G.: A combination framework for complexity. IC (to appear, 2016)
7.
Avanzini, M., Sternagel, C., Thiemann, R.: Certification of complexity proofs using CeTA. In: Proceeding of the 26th RTA, LIPIcs, vol. 36, pp. 23–39 (2015)
8.
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefMATH
9.
Bird, R.: Introduction to Functional Programming using Haskell, 2nd edn. Prentice Hall, Upper Saddle River (1998)
10.
Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Alternating runtime and size complexity analysis of integer programs. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 140–155. Springer, Heidelberg (2014)CrossRef
11.
Danner, N., Paykin, J., Royer, J.S.: A static cost analysis for a higher-order language. In: Proceeding of the 7th PLPV, pp. 25–34. ACM (2013)
12.
Gimenez, S., Moser, G.: The complexity of interaction. In: Proceeding of the 40th POPL (to appear, 2016)
13.
Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 364–379. Springer, Heidelberg (2008)CrossRef
14.
Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. TOPLAS 34(3), 14 (2012)CrossRefMATH
15.
Hofmann, M., Moser, G.: Multivariate amortised resource analysis for term rewrite systems. In: Proceeding of the 13th TLCA in LIPIcs Vol. 38, pp. 241–256 (2015)
16.
Jost, S., Hammond, K., Loidl, H.W., Hofmann, M.: Static determination of quantitative resource usage for higher-order programs. In: Proceeding of the 37th POPL, pp. 223–236. ACM (2010)
17.
Klein, G., Nipkow, T.: A machine-checked model for a java-like language, virtual machine, and compiler. TOPLAS 28(4), 619–695 (2006)CrossRef
18.
Lankford, D.: On Proving Term Rewriting Systems are Noetherian. Technical Report MTP-3. Louisiana Technical University (1979)
19.
Moser, G.: Proof Theory at Work: Complexity Analysis of Term Rewrite Systems. CoRR abs/0907.5527, Habilitation Thesis (2009)
20.
Moser, G., Schaper, M.: A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems (2012). CoRR, cs/PL/1204.1568, last revision: 6 May 2014
21.
Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. JAR 51(1), 27–56 (2013)MathSciNetCrossRefMATH
22.
Hill, P.M., Payet, E., Spoto, F.: Path-length analysis of object-oriented programs. In: Proceeding of the 1st EAAI. Elsevier (2006)
23.
24.
Reynolds, J.C.: Definitional interpreters for higher-order programming languages. HOSC 11(4), 363–397 (1998)MATH
25.
Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 745–761. Springer, Heidelberg (2014)
26.
TeReSe: Term Rewriting Systems, Cambridge Tracks in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)
27.
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenstrom, P.: The worst case execution time problem - overview of methods and survey of tools. TECS 7(3), 1–53 (2008)CrossRef
Metadata
Title
TcT: Tyrolean Complexity Tool
Authors
Martin Avanzini
Georg Moser
Michael Schaper
Copyright Year
2016
Publisher
Springer Berlin Heidelberg
Book
Tools and Algorithms for the Construction and Analysis of Systems

Print ISBN: 978-3-662-49673-2

Electronic ISBN: 978-3-662-49674-9

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-662-49674-9_24

Premium Partner

    Image Credits