article · 2008

Supplementing Java Bytecode with Specifications

Aleksy Schubert, Krzysztof Jakubczyk, Jędrzej Fulara

Cited by 0Abstract and details only

Abstract

The proof-carrying code (PCC) techniques allow the executable code to be augmented with a proof that the code obeys certain policies (e.g. the program does not store passwords in clear in a le). BML (Bytecode Modelling Language) can be regarded as a part of the PCC architecture which allows to express detailed properties of Java bytecode programs. As most of the programming is done at the source code level, it is desirable to have a way to translate properties expressed at the source code level (in our case written in Java Modeling Language, JML) to the bytecode level. In this paper we present a JML2BML compiler, a tool that for a given Java source le annotated with speci cations generates class les with BML.

Cite this paper

APA 7

Schubert, A., Jakubczyk, K., & Fulara, J. (2008). Supplementing Java Bytecode with Specifications.

MLA 9

Schubert, Aleksy, et al. “Supplementing Java Bytecode with Specifications.” 2008.

Chicago

Schubert, Aleksy, Krzysztof Jakubczyk, and Jędrzej Fulara. 2008. “Supplementing Java Bytecode with Specifications.”

Harvard

Schubert, A., Jakubczyk, K. and Fulara, J. (2008) ‘Supplementing Java Bytecode with Specifications’.

BibTeX

@article{schubert2008supplementing,
  title = {{Supplementing Java Bytecode with Specifications}},
  author = {Schubert, Aleksy and Jakubczyk, Krzysztof and Fulara, Jędrzej},
  year = {2008}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.