Verification of Programs via Intermediate Interpretation

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.

In Proceedings VPT 2017, arXiv:1708.06887. The author's extended version is arXiv:1705.06738

References in corpus (4)

• Turchin's Relation for Call-by-Name Computations: A Formal Approach
• A Note on Program Specialization. What Can Syntactical Properties of Residual Programs Reveal?
• Proceedings of the Fourth International Workshop on Verification and Program Transformation
• Generating Counterexamples for Model Checking by Transformation

Cited by in corpus (2)

• Optimizing Program Size Using Multi-result Supercompilation
• Controlling the Size of Supercompiled Programs using Multi-result Supercompilation