Verification of Programs via Intermediate Interpretation

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 safe...

Full description

Bibliographic Details
Main Authors: Alexei P. Lisitsa, Andrei P. Nemytykh
Format: Article
Language:English
Published: Open Publishing Association 2017-08-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1708.09002v1