Verification of Programs via Intermediate Interpretation

TL;DR

This paper presents a novel method for program verification using supercompilation of interpreters, enabling the proof of safety properties in functional programs modeling cache coherence protocols.

Contribution

It introduces a verification approach via intermediate interpretation and supercompilation, extending prior work by applying it to safety property proofs in functional programs.

Findings

Supercompilation successfully proved safety properties of cache coherence protocols.

The approach compares favorably with direct supercompilation verification methods.

Intermediate interpretation enhances the verification process.

Abstract

We explore an approach to verification of programs via program transformation applied to an interpreter of a programming language. A specialization technique known as Turchin's supercompilation is used to specialize some interpreters with respect to the program models. We show that several safety properties of functional programs modeling a class of cache coherence protocols can be proved by a supercompiler and compare the results with our earlier work on direct verification via supercompilation not using intermediate interpretation. Our approach was in part inspired by an earlier work by E. De Angelis et al. (2014-2015) where verification via program transformation and intermediate interpretation was studied in the context of specialization of constraint logic programs.