Systematic design of program transformation frameworks by abstract interpretation

Patrick Cousot; Radhia Cousot

doi:10.1145/503272.503290

Systematic design of program transformation frameworks by abstract interpretation

Patrick Cousot, Radhia Cousot

Computer Science

Research output: Contribution to journal › Conference article › peer-review

Abstract

We introduce a general uniform language-independent framework for designing online and offline source-to-source program transformations by abstract interpretation of program semantics. Iterative source-to-source program transformations are designed constructively by composition of source-to-semantics, semantics-to-transformed semantics and semantics-to-source abstractions applied to fixpoint trace semantics. The correctness of the transformations is expressed through observational and performance abstractions. The framework is illustrated on three examples: constant propagation, program specialization by online and offline partial evaluation and static program monitoring.

Original language	English (US)
Pages (from-to)	178-190
Number of pages	13
Journal	Conference Record of the Annual ACM Symposium on Principles of Programming Languages
DOIs	https://doi.org/10.1145/503272.503290
State	Published - 2002
Event	POPL 2002: 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Portland, OR, United States Duration: Jan 16 2002 → Jan 18 2002

ASJC Scopus subject areas

Software

Access to Document

10.1145/503272.503290

Cite this

@article{4a6de21ed66643f09bcd9c58ce41e951,

title = "Systematic design of program transformation frameworks by abstract interpretation",

abstract = "We introduce a general uniform language-independent framework for designing online and offline source-to-source program transformations by abstract interpretation of program semantics. Iterative source-to-source program transformations are designed constructively by composition of source-to-semantics, semantics-to-transformed semantics and semantics-to-source abstractions applied to fixpoint trace semantics. The correctness of the transformations is expressed through observational and performance abstractions. The framework is illustrated on three examples: constant propagation, program specialization by online and offline partial evaluation and static program monitoring.",

author = "Patrick Cousot and Radhia Cousot",

note = "Copyright: Copyright 2020 Elsevier B.V., All rights reserved.; POPL 2002: 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ; Conference date: 16-01-2002 Through 18-01-2002",

year = "2002",

doi = "10.1145/503272.503290",

language = "English (US)",

pages = "178--190",

journal = "Conference Record of the Annual ACM Symposium on Principles of Programming Languages",

issn = "0730-8566",

publisher = "Association for Computing Machinery (ACM)",

}

TY - JOUR

T1 - Systematic design of program transformation frameworks by abstract interpretation

AU - Cousot, Patrick

AU - Cousot, Radhia

PY - 2002

Y1 - 2002

N2 - We introduce a general uniform language-independent framework for designing online and offline source-to-source program transformations by abstract interpretation of program semantics. Iterative source-to-source program transformations are designed constructively by composition of source-to-semantics, semantics-to-transformed semantics and semantics-to-source abstractions applied to fixpoint trace semantics. The correctness of the transformations is expressed through observational and performance abstractions. The framework is illustrated on three examples: constant propagation, program specialization by online and offline partial evaluation and static program monitoring.

AB - We introduce a general uniform language-independent framework for designing online and offline source-to-source program transformations by abstract interpretation of program semantics. Iterative source-to-source program transformations are designed constructively by composition of source-to-semantics, semantics-to-transformed semantics and semantics-to-source abstractions applied to fixpoint trace semantics. The correctness of the transformations is expressed through observational and performance abstractions. The framework is illustrated on three examples: constant propagation, program specialization by online and offline partial evaluation and static program monitoring.

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

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

U2 - 10.1145/503272.503290

DO - 10.1145/503272.503290

M3 - Conference article

AN - SCOPUS:0036036551

SN - 0730-8566

SP - 178

EP - 190

JO - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

JF - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

T2 - POPL 2002: 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Y2 - 16 January 2002 through 18 January 2002

ER -

Systematic design of program transformation frameworks by abstract interpretation

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this