Abstract interpretation as anti-refinement
Programming Languages
2014-06-16 v2
Abstract
This article shows a correspondence between abstract interpretation of imperative programs and the refinement calculus: in the refinement calculus, an abstract interpretation of a program is a specification which is a function. This correspondence can be used to guide the design of mechanically verified static analyses, keeping the correctness proof well separated from the heuristic parts of the algorithms.
Cite
@article{arxiv.1310.4283,
title = {Abstract interpretation as anti-refinement},
author = {Arnaud Spiwack},
journal= {arXiv preprint arXiv:1310.4283},
year = {2014}
}
Comments
Working paper