Tags:formalization, Isabelle/HOL, simplification order and termination analysis
Abstract:
We present recent developments in CeTA w.r.t. the efficient certification of termination proofs. Here, efficiency is seen under various aspects. First, we present a case study on minimizing the formalization effort, namely when trying to verify the classical path orders by viewing them as instances of the weighted path order. Second, we argue that the efficient generation of certificates within termination tools requires more powerful certifiers, in particular when considering the usage of SAT- or SMT-solvers. Third, we present recent developments which aim at improving the execution time of CeTA.