Abstract
Common subexpression elimination (CSE) is a well-known method for code optimization in compilers. A key issue is the correctness of the program transformations performed. There are different versions of CSE but, to our knowledge, correctness proofs have not yet been published. The present paper contains a derivation of a version of CSE accompanied by a correctness proof based on the denotational semantics of the generated code.
| Original language | English |
|---|---|
| Pages (from-to) | 153-169 |
| Number of pages | 17 |
| Journal | Science of computer programming |
| Volume | 19 |
| Issue number | 2 |
| Publication status | Published - Nov-1992 |