Paper Info
Title
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.
Year
DOI
Venue
2017
10.4204/EPTCS.253.6
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Keywords
Field
DocType
program specialization, supercompilation, program analysis, program transformation, safety verification, cache coherence protocols
Program transformation,Programming language,Computer science,Theoretical computer science,Interpreter,Cache coherence
Journal
Volume
Issue
ISSN
abs/1705.06738
253
2075-2180
Citations 
PageRank 
References 
0
0.34
0
Authors
2
Name
Order
Citations
PageRank
Alexei Lisitsa127245.94
Andrei P. Nemytykh2938.50