μετα 2008

First International Workshop on Metacomputation in Russia
 

July 2-5, 2008, Pereslavl-Zalessky (120 km to the north-east from Moscow), Russia

Home
Call For Papers
Submissions
Accepted Papers
Program
Important Dates
Registration
Visa Support
Place
Affiliated Meetings
Contacts
Sponsors

 

 

 

 

An Experience with Term Rewriting for Program Verification

Sergei Mechveliani
 

Abstract

Full text pdf 219 KB

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.

Keywords:

automatic equational prover,
term rewriting,
inductive reasoning,
proof certificate.