Verifying Programs via Intermediate Interpretation

Lisitsa, Alexei P and Nemytykh, Andrei P (2017) Verifying Programs via Intermediate Interpretation. Electronic Proceedings in Theoretical Computer Science, EPTCS, 253. pp. 54-74.

Text 1705.06738v1.pdf - Submitted version Download (345kB)

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 De E. Angelis et al. (2014-2015) where verification via program transformation and intermediate interpretation was studied in the context of specialization of constraint logic programs.

Item Type:	Article
Additional Information:	Fifth International Workshop on Verification and Program Transformation (VPT-2017), April 29th, 2017, Uppsala, Sweden, 37 pages
Uncontrolled Keywords:	cs.PL, cs.PL
Depositing User:	Symplectic Admin
Date Deposited:	29 Aug 2017 10:06
Last Modified:	15 Mar 2024 04:46
DOI:	10.4204/EPTCS.253.6
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3009212