cl-banner

Termination Tools: Verification and Optimization


 Members
  • Aart Middeldorp
  • Christian Sternagel
  • Harald Zankl
FWF project number

P18763

  Contact

aart.middeldorp@uibk.ac.at

Publications

  • Challenges in Automation of Rewriting
    Harald Zankl
    Habilitation thesis, University of Innsbruck, 2014.
  • Modular Complexity Analysis for Term Rewriting
    Harald Zankl and Martin Korp
    Logical Methods in Computer Science 10(1:19), pp. 1 – 33, 2014.
  • Uncurrying for Termination and Complexity
    Nao Hirokawa, Aart Middeldorp, and Harald Zankl
    Journal of Automated Reasoning 50(3), pp. 279 – 315, 2013.
  • Uncurrying for Innermost Termination and Derivational Complexity
    Harald Zankl, Nao Hirokawa, and Aart Middeldorp
    Proceedings of the 5th International Workshop on Higher-Order Rewriting (HOR 2010), Electronic Proceedings in Theoretical Computer Science 49, pp. 46 – 57, 2011.
  • Automatic Certification of Termination Proofs
    Christian Sternagel
    PhD thesis, University of Innsbruck, 2010.
  • Signature Extensions Preserve Termination – An Alternative Proof via Dependency Pairs
    Christian Sternagel and René Thiemann
    Proceedings of the 19th Annual Conference of the European Association for Computer Science Logic (CSL 2010), Lecture Notes in Computer Science 6247, pp. 514 – 528, 2010.
  • Modular Complexity Analysis via Relative Complexity
    Harald Zankl and Martin Korp
    Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 385 – 400, 2010.
  • Certified Subterm Criterion and Certified Usable Rules
    Christian Sternagel and René Thiemann
    Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 325 – 340, 2010.
  • Satisfiability of Non-Linear (Ir)rational Arithmetic
    Harald Zankl and Aart Middeldorp
    Proceedings of the 16th International Conference on Logic for Programming and Automated Reasoning (LPAR-16), Lecture Notes in Artificial Intelligence 6355, pp. 481 – 500, 2010.
  • Finding and Certifying Loops
    Harald Zankl, Christian Sternagel, Dieter Hofbauer, and Aart Middeldorp
    Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2010), Lecture Notes in Computer Science 5901, pp. 755 – 766, 2010.
  • Lazy Termination Analysis
    Harald Zankl
    PhD thesis, University of Innsbruck, 2009.
  • Increasing interpretations
    Harald Zankl and Aart Middeldorp
    Annals of Mathematics and Artificial Intelligence 56(1), pp. 87 – 108, 2009.
  • Certification of Termination Proofs using CeTA
    René Thiemann and Christian Sternagel
    Proceedings of the 22nd International Conference on Theorem Proving in Higher-Order Logics (TPHOLs 2009), Lecture Notes in Computer Science 5674, pp. 452 – 468, 2009.
  • Transforming SAT into Termination of Rewriting
    Harald Zankl, Christian Sternagel, and Aart Middeldorp
    Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008), Electronic Notes in Theoretical Computer Science 246, pp. 199 – 214, 2009.
  • KBO Orientability
    Harald Zankl, Nao Hirokawa, and Aart Middeldorp
    Journal of Automated Reasoning 43(2), pp. 173 – 201, 2009.
  • Loops under Strategies
    René Thiemann and Christian Sternagel
    Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 17 – 31, 2009.
  • Tyrolean Termination Tool 2
    Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp
    Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 295 – 304, 2009.
  • From Outermost Termination to Innermost Termination
    René Thiemann
    Proceedings of the 35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2009), Lecture Notes in Computer Science 5404, pp. 533 – 545, 2009.
  • Uncurrying for Termination
    Nao Hirokawa, Aart Middeldorp, and Harald Zankl
    Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), Lecture Notes in Artificial Intelligence 5330, pp. 667 – 681, 2008.
  • Increasing Interpretations
    Harald Zankl and Aart Middeldorp
    Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2008), Lecture Notes in Artificial Intelligence 5144, pp. 191 – 205, 2008.
  • Root-Labeling
    Christian Sternagel and Aart Middeldorp
    Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 336 – 350, 2008.
  • Maximal Termination
    Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl
    Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 110 – 125, 2008.
  • Innermost Termination of Rewrite Systems by Labeling
    René Thiemann and Aart Middeldorp
    Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), Electronic Notes in Theoretical Computer Science 204, pp. 3 – 19, 2008.
  • Predictive Labeling with Dependency Pairs using SAT
    Adam Koprowski and Aart Middeldorp
    Proceedings of the 21st International Conference on Automated Deduction (CADE 2007), Lecture Notes in Artificial Intelligence 4603, pp. 410 – 425, 2007.
  • Satisfying KBO Constraints
    Harald Zankl and Aart Middeldorp
    Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007), Lecture Notes in Computer Science 4533, pp. 389 – 403, 2007.
  • SAT Solving for Termination Analysis with Polynomial Interpretations
    Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl
    Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), Lecture Notes in Computer Science 4501, pp. 340 – 254, 2007.
  • Tyrolean Termination Tool: Techniques and Features
    Nao Hirokawa and Aart Middeldorp
    Information and Computation 205(4), pp. 474 – 511, 2007.
  • Constraints for Argument Filterings
    Harald Zankl, Nao Hirokawa, and Aart Middeldorp
    Proceedings of the 33rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2007), Lecture Notes in Computer Science 4362, pp. 579 – 590, 2007.
  • Uncurrying for Termination
    Nao Hirokawa and Aart Middeldorp
    Proceedings of the 3rd International Workshop on Higher-Order Rewriting (HOR 2006),   pp. 19 – 24, 2006.
  • Predictive Labeling
    Nao Hirokawa and Aart Middeldorp
    Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA 2006), Lecture Notes in Computer Science 4098, pp. 313 – 327, 2006.
Nach oben scrollen