Verification tools in the development of provably correct compilers

Abstract

The paper presents a practical verification tool that helps in the development of provably correct compilers. The tool is based on the approach of proving termination of PROLOG-like programs using term-rewriting techniques and a technique of testing whether a given PROLOG program can be soundly executed on PROLOG interpreters without the Occur-check test. The tool has been built on top of the theorem prover, RRL (Rewrite Rule Laboratory). The tool is effective for compilers developed using Hoare’s refinement algebra approach. The utility of the tool is illustrated through a case study on correctness of a prototype compiler of the ProCoS level 0 language PL0.