*Result*: Preservation of Proof Obligations from Java to the Java Virtual Machine.
*Further Information*
*While program verification environments typically target source programs, there is an increasing need to provide strong guarantees for executable programs. We establish that it is possible to reuse the proof that a source Java program meets its specification to show that the corresponding JVM program, obtained by non-optimizing compilation, meets the same specification. More concretely, we show that verification condition generators for Java and JVM programs generate the same set of proof obligations, when applied to a program p and its compilation [[p]] respectively. Preservation of proof obligations extends the applicability of Proof Carrying Code, by allowing certificate generation to rely on existing verification technology. [ABSTRACT FROM AUTHOR]
Copyright of Automated Reasoning (9783540710691) is the property of Springer Nature / Books and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)*