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

Jan Midtgaard, Michael Adams, and Matthew Might

Status: Published


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 composition of Galois connections and thus rests on the foundations of abstract interpretation.


Computer Science


Jan Midtgaard, Michael Adams, and Matthew Might. A structural soundness proof for Shiverss escape technique: A case for Galois connections. In Antoine Miné and David Schmidt, editors, Static Analysis, volume 7460 of Lecture Notes in Computer Science, pages 352–369. Springer Berlin / Heidelberg, 2012. ISBN 978-3-642-33124-4. ISSN 0302-9743 (Print) 1611-3349 (Online). doi: 10.1007/978-3-642-33125-1_24.

BibTeX Entry

  author = {Midtgaard, Jan and Adams, Michael and Might, Matthew},
  title = {A Structural Soundness Proof for {S}hivers{\textquoteright}s Escape Technique: A Case for {G}alois Connections},
  booktitle = {Static Analysis},
  pages = {352--369},
  year = {2012},
  editor = {Min{\'e}, Antoine and Schmidt, David},
  volume = {7460},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {978-3-642-33124-4},
  issn = {0302-9743 (Print) 1611-3349 (Online)},
  doi = {10.1007/978-3-642-33125-1_24},

Copyright Notice

This is a self-archived, author-created version of the work.The original publication is available at www.springerlink.com.