A case study in abstract interpretation based program transformation

Blocking command elimination

Patrick Cousot, Radhia Cousot

Research output: Contribution to journalArticle

Abstract

The design of correct semantics-based program transformations was illustrated using abstract interpretation on blocking code elimination. The general idea to formalize program transformation by abstract interpretation was to define a semantic transformation as an abstraction of the subject program semantics. The correctness of the semantic transformation is proved using an observational abstraction and specify details about the subject and transformed semantics should be abstracted away to considered them as equivalent. It is stated that abstract interpretation can be used to define a semantics-based program transformation framework.

Original languageEnglish (US)
Pages (from-to)45-68
Number of pages24
JournalElectronic Notes in Theoretical Computer Science
Volume45
DOIs
StatePublished - Nov 2001

Fingerprint

Program Transformation
Abstract Interpretation
Elimination
Semantics
Correctness

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

@article{aa3e30fe35174e27a65114334a9b19dc,
title = "A case study in abstract interpretation based program transformation: Blocking command elimination",
abstract = "The design of correct semantics-based program transformations was illustrated using abstract interpretation on blocking code elimination. The general idea to formalize program transformation by abstract interpretation was to define a semantic transformation as an abstraction of the subject program semantics. The correctness of the semantic transformation is proved using an observational abstraction and specify details about the subject and transformed semantics should be abstracted away to considered them as equivalent. It is stated that abstract interpretation can be used to define a semantics-based program transformation framework.",
author = "Patrick Cousot and Radhia Cousot",
year = "2001",
month = "11",
doi = "10.1016/S1571-0661(04)80954-X",
language = "English (US)",
volume = "45",
pages = "45--68",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - A case study in abstract interpretation based program transformation

T2 - Blocking command elimination

AU - Cousot, Patrick

AU - Cousot, Radhia

PY - 2001/11

Y1 - 2001/11

N2 - The design of correct semantics-based program transformations was illustrated using abstract interpretation on blocking code elimination. The general idea to formalize program transformation by abstract interpretation was to define a semantic transformation as an abstraction of the subject program semantics. The correctness of the semantic transformation is proved using an observational abstraction and specify details about the subject and transformed semantics should be abstracted away to considered them as equivalent. It is stated that abstract interpretation can be used to define a semantics-based program transformation framework.

AB - The design of correct semantics-based program transformations was illustrated using abstract interpretation on blocking code elimination. The general idea to formalize program transformation by abstract interpretation was to define a semantic transformation as an abstraction of the subject program semantics. The correctness of the semantic transformation is proved using an observational abstraction and specify details about the subject and transformed semantics should be abstracted away to considered them as equivalent. It is stated that abstract interpretation can be used to define a semantics-based program transformation framework.

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

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

U2 - 10.1016/S1571-0661(04)80954-X

DO - 10.1016/S1571-0661(04)80954-X

M3 - Article

VL - 45

SP - 45

EP - 68

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -