A calculational approach to control-flow analysis by abstract interpretation

Jan Midtgaard*, Thomas Jensen

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Resumé

We present a derivation of a control-flow analysis by abstract interpretation. Our starting point is a transition system semantics defined as an abstract machine for a small functional language in continuation-passing style. We obtain a Galois connection for abstracting the machine states by composing Galois connections, most notable an independent-attribute Galois connection on machine states and a Galois connection induced by a closure operator associated with a constituent-parts relation on environments. We calculate abstract transfer functions by applying the state abstraction to the collecting semantics, resulting in a novel characterization of demand-driven 0-CFA.

OriginalsprogEngelsk
TitelStatic Analysis - 15th International Symposium, SAS 2008, Proceedings
Antal sider16
Publikationsdato13. aug. 2008
Sider347-362
ISBN (Trykt)3540691634, 9783540691631
DOI
StatusUdgivet - 13. aug. 2008
Begivenhed15th International Static Analysis Symposium, SAS 2008 - Valencia, Spanien
Varighed: 16. jul. 200818. jul. 2008

Konference

Konference15th International Static Analysis Symposium, SAS 2008
LandSpanien
ByValencia
Periode16/07/200818/07/2008
SponsorEAPLS, ERCIM, Generalitat Valenciana, MEC (Feder) TIN2007-30509-E, Polytechnic University of Valencia
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind5079 LNCS
ISSN0302-9743

Fingeraftryk

semantics
transfer functions
closures
derivation
operators

Citer dette

Midtgaard, J., & Jensen, T. (2008). A calculational approach to control-flow analysis by abstract interpretation. I Static Analysis - 15th International Symposium, SAS 2008, Proceedings (s. 347-362). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind. 5079 LNCS https://doi.org/10.1007/978-3-540-69166-2_23
Midtgaard, Jan ; Jensen, Thomas. / A calculational approach to control-flow analysis by abstract interpretation. Static Analysis - 15th International Symposium, SAS 2008, Proceedings. 2008. s. 347-362 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 5079 LNCS).
@inproceedings{79ee00ab60674fea8af30296f8a94a2d,
title = "A calculational approach to control-flow analysis by abstract interpretation",
abstract = "We present a derivation of a control-flow analysis by abstract interpretation. Our starting point is a transition system semantics defined as an abstract machine for a small functional language in continuation-passing style. We obtain a Galois connection for abstracting the machine states by composing Galois connections, most notable an independent-attribute Galois connection on machine states and a Galois connection induced by a closure operator associated with a constituent-parts relation on environments. We calculate abstract transfer functions by applying the state abstraction to the collecting semantics, resulting in a novel characterization of demand-driven 0-CFA.",
author = "Jan Midtgaard and Thomas Jensen",
year = "2008",
month = "8",
day = "13",
doi = "10.1007/978-3-540-69166-2_23",
language = "English",
isbn = "3540691634",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Heinemann",
pages = "347--362",
booktitle = "Static Analysis - 15th International Symposium, SAS 2008, Proceedings",

}

Midtgaard, J & Jensen, T 2008, A calculational approach to control-flow analysis by abstract interpretation. i Static Analysis - 15th International Symposium, SAS 2008, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 5079 LNCS, s. 347-362, 15th International Static Analysis Symposium, SAS 2008, Valencia, Spanien, 16/07/2008. https://doi.org/10.1007/978-3-540-69166-2_23

A calculational approach to control-flow analysis by abstract interpretation. / Midtgaard, Jan; Jensen, Thomas.

Static Analysis - 15th International Symposium, SAS 2008, Proceedings. 2008. s. 347-362 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 5079 LNCS).

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

TY - GEN

T1 - A calculational approach to control-flow analysis by abstract interpretation

AU - Midtgaard, Jan

AU - Jensen, Thomas

PY - 2008/8/13

Y1 - 2008/8/13

N2 - We present a derivation of a control-flow analysis by abstract interpretation. Our starting point is a transition system semantics defined as an abstract machine for a small functional language in continuation-passing style. We obtain a Galois connection for abstracting the machine states by composing Galois connections, most notable an independent-attribute Galois connection on machine states and a Galois connection induced by a closure operator associated with a constituent-parts relation on environments. We calculate abstract transfer functions by applying the state abstraction to the collecting semantics, resulting in a novel characterization of demand-driven 0-CFA.

AB - We present a derivation of a control-flow analysis by abstract interpretation. Our starting point is a transition system semantics defined as an abstract machine for a small functional language in continuation-passing style. We obtain a Galois connection for abstracting the machine states by composing Galois connections, most notable an independent-attribute Galois connection on machine states and a Galois connection induced by a closure operator associated with a constituent-parts relation on environments. We calculate abstract transfer functions by applying the state abstraction to the collecting semantics, resulting in a novel characterization of demand-driven 0-CFA.

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

U2 - 10.1007/978-3-540-69166-2_23

DO - 10.1007/978-3-540-69166-2_23

M3 - Article in proceedings

AN - SCOPUS:48949094503

SN - 3540691634

SN - 9783540691631

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 347

EP - 362

BT - Static Analysis - 15th International Symposium, SAS 2008, Proceedings

ER -

Midtgaard J, Jensen T. A calculational approach to control-flow analysis by abstract interpretation. I Static Analysis - 15th International Symposium, SAS 2008, Proceedings. 2008. s. 347-362. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 5079 LNCS). https://doi.org/10.1007/978-3-540-69166-2_23