Ehud Altman, Kenneth R. Brown, et al.
PRX Quantum
In this paper, we show how refinement calculus provides a basis for translation validation of optimized programs written in high level languages. Towards such a direction, we shall provide a generalized proof rule for establishing refinement of source and target programs for which one need not have to know the underlying program transformations. Our method is supported by a semi-automatic tool that uses a theorem prover for validating the verification conditions. We further show that the translation validation infrastructure provides an effective basis for deriving semantic debuggers and illustrate the development of a simple debugger for optimized programs using this approach using Prolog. A distinct advantage of semantic debugging is that it permits the user to change values at run-time only when the values are consistent with the underlying semantics. © 2005 Elsevier B.V. All rights reserved.
Ehud Altman, Kenneth R. Brown, et al.
PRX Quantum
Kafai Lai, Alan E. Rosenbluth, et al.
SPIE Advanced Lithography 2007
Rafae Bhatti, Elisa Bertino, et al.
Communications of the ACM
Donald Samuels, Ian Stobert
SPIE Photomask Technology + EUV Lithography 2007