(1 + ε)-approximate sparse recovery
Eric Price, David P. Woodruff
FOCS 2011
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.
Eric Price, David P. Woodruff
FOCS 2011
Bowen Zhou, Bing Xiang, et al.
SSST 2008
Israel Cidon, Leonidas Georgiadis, et al.
IEEE/ACM Transactions on Networking
Michael Ray, Yves C. Martin
Proceedings of SPIE - The International Society for Optical Engineering