An Isabelle/HOL Formalization of Rewriting 
for Certified Tool Assertions 


On this page we provide detailed links to our formalization and experimental evidence concerning our paper Certification of Complexity Proofs using CeTA.


Theories mentioned in the papers

Definitions and theorems of the paper


As testbed we used the runtime complexity testsuite from the termination problem data base, version 9.0.2, which also served as testbed for the complexity category of the FLoC Olympic Games of 2014. All tests were conducted on a machine with a 8 dual core AMD Opteron 885 processors running at 2.60GHz with 64Gb of RAM, within a timeout of 60 seconds per test.

We have conducted the following tests: