Termination Tools: Verification and Optimization

Members

• Aart Middeldorp
• Christian Sternagel
• Harald Zankl

FWF project number

Contact

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.