Informatics Report Series


Report   

EDI-INF-RR-0509


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Optimisation Validation
Authors: David Aspinall ; Beringer Lennart ; Alberto Momigliano
Date:Dec 2005
Publication Title:COCV 2006
Abstract:
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 setting is within a program logic framework for a subset of Java bytecode, which is complete for a resource-annotated operational semantics based on resource algebras endowed with a cost ordering. We describe examples of optimisation validation that we have formally verified (in Isabelle/HOL) using the logic and we also introduce a static type and effect system which is in certain cases useful for showing optimisation validation without needing the logic.
Links To Paper
1st Link
Bibtex format
@Misc{EDI-INF-RR-0509,
author = { David Aspinall and Beringer Lennart and Alberto Momigliano },
title = {Optimisation Validation},
year = 2005,
month = {Dec},
url = {http://homepages.inf.ed.ac.uk/amomigl1/papers/OptVal.pdf},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh