An Experience with Term Rewriting for Program Verification

We have developed a proof assistant based on many-sorted term rewriting, unfailing completion, and inductive reasoning. We are going to interface it to our computer algebra library. Its application also includes automated program and digital device analysis. It also can be used for generating certificates for proofs and programs, with automatic certificate check. The system and the CA library are implemented in the Haskell language.