A structural soundness proof for Shivers’s escape technique a case for Galois connections

Jan Midtgaard, Michael D. Adams, Matthew Might

Research output: Contribution to journalConference articleResearchpeer-review

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

Original languageEnglish
Book seriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7460 LNCS
ISSN0302-9743
DOIs
Publication statusPublished - 1. Jan 2012
Event19th International Static Analysis Symposium, SAS 2012 - Deauville, France
Duration: 11. Sep 201213. Sep 2012

Conference

Conference19th International Static Analysis Symposium, SAS 2012
CountryFrance
CityDeauville
Period11/09/201213/09/2012
SponsorCNRS - The National Center for Scientific Research, École Normale Supérieure, French Institute for Research in Computer Science and Automation

Fingerprint

Galois Connection
Soundness
Flow control
Abstract Interpretation
Flow Control
Chemical analysis
Fragment
Higher Order

Cite this

@inproceedings{28e31300730044d4aa077e66bab28327,
title = "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 composition of Galois connections and thus rests on the foundations of abstract interpretation.",
author = "Jan Midtgaard and Adams, {Michael D.} and Matthew Might",
year = "2012",
month = "1",
day = "1",
doi = "10.1007/978-3-642-33125-1_24",
language = "English",
volume = "7460 LNCS",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Heinemann",

}

A structural soundness proof for Shivers’s escape technique a case for Galois connections. / Midtgaard, Jan; Adams, Michael D.; Might, Matthew.

In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7460 LNCS, 01.01.2012.

Research output: Contribution to journalConference articleResearchpeer-review

TY - GEN

T1 - A structural soundness proof for Shivers’s escape technique a case for Galois connections

AU - Midtgaard, Jan

AU - Adams, Michael D.

AU - Might, Matthew

PY - 2012/1/1

Y1 - 2012/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84982160646&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-33125-1_24

DO - 10.1007/978-3-642-33125-1_24

M3 - Conference article

AN - SCOPUS:84982160646

VL - 7460 LNCS

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -