Optimisation Validation | Zendy

David Aspinall | Zendy; Lennart Beringer | Zendy; Alberto Momigliano | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Optimisation Validation

Author(s) -

David Aspinall,

Lennart Beringer,

Alberto Momigliano

Publication year - 2007

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2006.06.017

Subject(s) - computer science , hol , java bytecode , programming language , operational semantics , semantics (computer science) , compiler , transformation (genetics) , program transformation , bytecode , abstract interpretation , java , theoretical computer science , biochemistry , chemistry , java applet , java annotation , gene

We introduce the idea of optimisation validation, which is to formally establish that an instance of an optimising transformation indeed improves with respect to some resource measure. This is related to, but in contrast with, translation validation, which aims to establish that a particular instance of a transformation undertaken by an optimising compiler is semantics preserving. Our main setting is a program logic for a subset of Java bytecode, which is sound and complete for a resource-annotated operational semantics. The latter employs resource algebras for measuring dynamic costs such as time, space and more elaborate examples. We describe examples of optimisation validation that we have formally verified in Isabelle/HOL using the logic. We also introduce a type and effect system for measuring static costs such as code size, which is proved consistent with the operational semantics

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research