Abstract interpretation as anti-refinement
Arnaud Spiwack
TL;DR
This paper establishes a correspondence between abstract interpretation and the refinement calculus, enabling the design of verified static analyses with clear separation of correctness proofs from heuristics.
Contribution
It introduces a novel link between abstract interpretation and refinement calculus, aiding the development of mechanically verified static analysis tools.
Findings
Abstract interpretation can be viewed as a specification in the refinement calculus.
The correspondence facilitates correctness proofs separate from heuristic algorithm parts.
Guides the design of verified static analysis algorithms.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Security and Verification in Computing