BML and Related Tools

The Bytecode Modeling Language (BML) is a specication for Java bytecode, that provides a high level of abstraction, while not restricting the format of the bytecode. Notably, BML specications can be stored in class les, so that they can be shipped together with the bytecode. This makes BML particularly suited as property specication language in a proof-carrying code framework. Moreover, BML is designed to be close to the source code level specication language JML, so that specications (and proofs) developed at the more intuitive source code level can be compiled into bytecode level. This paper describes the BML language and its binary representation. It also discusses the tool set that is available to support BML, containing BMLLib, a library to inspect and edit BML specications; Umbra, a BML viewer and editor, integrated in Eclipse; JML2BML, a compiler from JML to BML specications; BML2BPL, a translator from BML to BoogiePL, so that the BoogiePL verication condition generator can be ...

• Type: Conference
• Year: 2008
• Where: FMCO
• Authors: Jacek Chrzaszcz, Marieke Huisman, Aleksy Schubert
• Keywords: BML Language, BML Specications, FMCO 2008, Formal Methods, Source Code Level