A Structural Soundness Proof for Shivers's Escape Technique - A Case for Galois Connections

Abstract. Shivers’s escape technique enables one to analyse the control flow of higher-order program fragments. It is widely used, but its soundness has never been proven. In this paper, we present the first soundness proof for the technique. Our proof is structured as a composiGalois connections and thus rests on the foundations of abstract interpretation.

• Type: Journal
• Year: 2012
• Where: SAS
• Authors: Jan Midtgaard, Michael D. Adams 0001, Matthew Might
• Keywords: Abstract Interpretation, Formal Methods, Program Fragments, SAS 2012, Soundness