Resumé
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.
| Originalsprog | Engelsk |
|---|---|
| Bogserie | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Vol/bind | 7460 LNCS |
| ISSN | 0302-9743 |
| DOI | |
| Status | Udgivet - 1. jan. 2012 |
| Begivenhed | 19th International Static Analysis Symposium, SAS 2012 - Deauville, Frankrig Varighed: 11. sep. 2012 → 13. sep. 2012 |
Konference
| Konference | 19th International Static Analysis Symposium, SAS 2012 |
|---|---|
| Land | Frankrig |
| By | Deauville |
| Periode | 11/09/2012 → 13/09/2012 |
| Sponsor | CNRS - The National Center for Scientific Research, École Normale Supérieure, Institut National de Recherche en Informatique et en Automatique |
Fingeraftryk
Citer dette
}
A structural soundness proof for Shivers’s escape technique a case for Galois connections. / Midtgaard, Jan; Adams, Michael D.; Might, Matthew.
I: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 7460 LNCS, 01.01.2012.Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › peer 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 -