Paper Info
Title
Finite Countermodel Based Verification For Program Transformation (A Case Study)
Abstract
Both automatic program verification and program transformation are based on program analysis. In the past decade a number of approaches using various automatic general-purpose program transformation techniques (partial deduction, specialization, supercompilation) for verification of unreachability properties of computing systems were introduced and demonstrated [10, 19, 30, 36]. On the other hand, the semantics based unfold-fold program transformation methods pose themselves diverse kinds of reachability tasks and try to solve them, aiming at improving the semantics tree of the program being transformed. That means some general-purpose verification methods may be used for strengthening program transformation techniques. This paper considers the question how finite countermodels for safety verification method [34] might be used in Turchin's supercompilation method. We extract a number of supercompilation sub-algorithms trying to solve reachability problems and demonstrate use of an external model finder for solving some of the problems.
Year
DOI
Venue
2015
10.4204/EPTCS.199.2
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Keywords
DocType
Issue
program specialization, supercompilation, program analysis, program transformation, safety verification, finite countermodels
Journal
199
ISSN
Citations 
PageRank 
2075-2180
0
0.34
References 
Authors
25
2
Name
Order
Citations
PageRank
Alexei Lisitsa127245.94
Andrei P. Nemytykh2938.50