Using the HOL prove assistant for proving the correctness of term rewriting rules reducing terms of sequential behavior

Abstract

There are several approaches of using automated theorem provers and assistants in hardware verification. It has been shown, that hardware behavior can be modelled and verified using theorem proving tools. But the task of generating a proof remains difficult and often needs a big amount of interaction. Therefore, the methods of our hardware verification system VERENA are based on term rewriting. It is shown how we use the expressive power of type theory to model circuit behavior. The crucial point in implementing a term rewriting system is to guarantee that the term rewriting rules used have specific properties like correctness, confluence, completeness, etc. It is demonstrated how we use the HOL prove assistant to prove the correctness of term rewriting rules.