Browsing School of Electronic Engineering and Computer Science by Author "Thiemann, R"

Now showing items 1-4 of 4

    • Certification of Confluence Proofs using CeTA 

      Nagele, J; Thiemann, R; 3rd International Workshop on Confluence (2014-07-13)
      CeTA was originally developed as a tool for certifying termination proofs which have to be provided as certificates in the CPF-format. Its soundness is proven as part of IsaFoR, the Isabelle Formalization of Rewriting. By ...

    • Certification of nontermination proofs using strategies and nonlooping derivations 

      Nagele, J; Thiemann, R; Winkler, S; 6th Working Conference on Verified Software: Theories, Tools, and Experiments (2014-10-14)
      © 2014 Springer International Publishing Switzerland. The development of sophisticated termination criteria for term rewrite systems has led to powerful and complex tools that produce (non)termination proofs automatically. ...

    • On the formalization of termination techniques based on multiset orderings 

      Thiemann, R; Allais, G; Nagele, J; 23rd International Conference on Rewriting Techniques and Applications (Leibniz International Proceedings in Informatics, LIPIcs, 2012)
      Multiset orderings are a key ingredient in certain termination techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination ...

    • On the formalization of termination techniques based on multiset orderings 

      Thiemann, R; Allais, G; Nagele, J; 23rd International Conference on Rewriting Techniques and Applications (2012-12-01)
      Multiset orderings are a key ingredient in certain termination techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination ...