Automated Implicit Computational Complexity Analysis (System Description)

1. Marion, J.Y., Moyen, J.Y.: Efficient first order functional program interpreter with time bound certifications. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 25–42. Springer, Heidelberg (2000)

   Google Scholar 

2. Bonfante, G., Cichon, A., Marion, J.Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. JFP 11(1), 33–53 (2001)

   Article  MATH  MathSciNet  Google Scholar 

3. Marion, J.Y.: Analysing the implicit complexity of programs. IC 183, 2–18 (2003)

   MATH  MathSciNet  Google Scholar 

4. Marion, J.Y., Péchoux, R.: Resource analysis by sup-interpretation. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, pp. 163–176. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

5. Marion, J.Y., Péchoux, R.: Quasi-friendly sup-interpretations. CoRR abs/cs/0608020 (2006)

   Google Scholar 

6. Avanzini, M., Moser, G.: Complexity analysis by rewriting. In: Proc. 9th FLOPS. LNCS, vol. 4989, pp. 130–146. Springer, Heidelberg (2008)

   Google Scholar 

7. Bonfante, G., Marion, J.Y., Moyen, J.Y.: Quasi-intepretations and small space bounds. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 150–164. Springer, Heidelberg (2005)

   Google Scholar 

8. Bonfante, G., Marion, J.Y., Péchoux, R.: Quasi-interpretation synthesis by decomposition. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 410–424. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

9. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

   Google Scholar 

10. Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 167–177. Springer, Heidelberg (1989)

    Google Scholar 

11. Steinbach, J.: Generating polynomial orderings. IPL 49, 85–93 (1994)

    Article  MATH  Google Scholar 

12. Zantema, H.: Termination of term rewriting by semantic labelling. FI 24, 89–105 (1995)

    MATH  MathSciNet  Google Scholar 

13. Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: Proc. 19th RTA 2008. LNCS, vol. 5117 (to appear, 2008)

    Google Scholar 

14. Contejean, E., Marché, C., Tomás, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. JAR 34(4), 325–363 (2005)

    Article  MATH  Google Scholar 

15. Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

16. Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M., Giesl, J.: Proving termination using recursive path orders and SAT solving. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 267–282. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

17. Steinbach, J., Kühler, U.: Check your ordering - termination proofs and open problems. Technical Report SR-90-25, University of Kaiserslautern (1990)

    Google Scholar 

18. Dershowitz, N.: 33 examples of termination. In: Term Rewriting, French Spring School of Theoretical Computer Science, Advanced Course, pp. 16–26. Springer, Heidelberg (1995)

    Google Scholar 

19. Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical Report AIB-09-2001, RWTH Aachen (2001)

    Google Scholar 

20. Moser, G., Schnabl, A.: Proving quadratic derivational complexities using context dependent interpretations. In: Proc. 19th RTA 2008. LNCS, vol. 5117 (to appear, 2008)

    Google Scholar 

Download references