An Isabelle/HOL Formalization of Rewriting 
for Certified Tool Assertions 

General

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

Links

Theories mentioned in the papers

Definitions and theorems of the paper

Experiments

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: