BML and Related Tools

J. Chrząszcz; Marieke Huisman; A. Schubert

doi:10.1007/978-3-642-04167-9_14

BML and Related Tools

J. Chrząszcz, Marieke Huisman, A. Schubert

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

Abstract

The Bytecode Modeling Language (BML) is a specification language for Java bytecode, that provides a high level of abstraction, while not restricting the format of the bytecode. Notably, BML specifications can be stored in class files, so that they can be shipped together with the bytecode. This makes BML particularly suited as property specification language in a proof-carrying code framework. Moreover, BML is designed to be close to the source code level specification language JML, so that specifications (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 specifications; Umbra, a BML viewer and editor, integrated in Eclipse; JML2BML, a compiler from JML to BML specifications; BMLt2BPL, a translator from BML to BoogiePL, so that the BoogiePL verification condition generator can be used; and CCT, a tool to store proofs in class files.

Original language	Undefined
Title of host publication	Formal Methods for Components and Objects
Editors	F.S de Boer, M.M. Bonsangue, E. Madelaine
Place of Publication	London
Publisher	Springer
Pages	278-297
Number of pages	20
ISBN (Print)	978-3-642-04166-2
DOIs	https://doi.org/10.1007/978-3-642-04167-9_14
Publication status	Published - 2009
Event	Formal Methods for Components and Objects - Sophia Antipolis, France Duration: 21 Oct 2008 → 23 Oct 2008

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	5751

Conference

Conference	Formal Methods for Components and Objects
Period	21/10/08 → 23/10/08
Other	21-23 Oktober 2008

Keywords

METIS-263979
IR-67853
Program Verification
tool support
proof carrying code
Specification
Verification
EWI-15929
bytecode

Access to Document

10.1007/978-3-642-04167-9_14

http://eprints.eemcs.utwente.nl/secure2/15929/01/fulltext.pdf

Cite this

@inproceedings{724bd92a01c44a89a517a2958b7264f6,

title = "BML and Related Tools",

abstract = "The Bytecode Modeling Language (BML) is a specification language for Java bytecode, that provides a high level of abstraction, while not restricting the format of the bytecode. Notably, BML specifications can be stored in class files, so that they can be shipped together with the bytecode. This makes BML particularly suited as property specification language in a proof-carrying code framework. Moreover, BML is designed to be close to the source code level specification language JML, so that specifications (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 specifications; Umbra, a BML viewer and editor, integrated in Eclipse; JML2BML, a compiler from JML to BML specifications; BMLt2BPL, a translator from BML to BoogiePL, so that the BoogiePL verification condition generator can be used; and CCT, a tool to store proofs in class files.",

keywords = "METIS-263979, IR-67853, Program Verification, tool support, proof carrying code, Specification, Verification, EWI-15929, bytecode",

author = "J. Chrz{\c a}szcz and Marieke Huisman and A. Schubert",

note = "Work done in the context of the IST-FET-2005-015905 Mobius project.; null ; Conference date: 21-10-2008 Through 23-10-2008",

year = "2009",

doi = "10.1007/978-3-642-04167-9_14",

language = "Undefined",

isbn = "978-3-642-04166-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "278--297",

editor = "{de Boer}, F.S and M.M. Bonsangue and E. Madelaine",

booktitle = "Formal Methods for Components and Objects",

}

BML and Related Tools. / Chrząszcz, J.; Huisman, Marieke; Schubert, A.

Formal Methods for Components and Objects. ed. / F.S de Boer; M.M. Bonsangue; E. Madelaine. London : Springer, 2009. p. 278-297 10.1007/978-3-642-04167-9_14 (Lecture Notes in Computer Science; Vol. 5751).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - BML and Related Tools

AU - Chrząszcz, J.

AU - Huisman, Marieke

AU - Schubert, A.

N1 - Work done in the context of the IST-FET-2005-015905 Mobius project.

PY - 2009

Y1 - 2009

N2 - The Bytecode Modeling Language (BML) is a specification language for Java bytecode, that provides a high level of abstraction, while not restricting the format of the bytecode. Notably, BML specifications can be stored in class files, so that they can be shipped together with the bytecode. This makes BML particularly suited as property specification language in a proof-carrying code framework. Moreover, BML is designed to be close to the source code level specification language JML, so that specifications (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 specifications; Umbra, a BML viewer and editor, integrated in Eclipse; JML2BML, a compiler from JML to BML specifications; BMLt2BPL, a translator from BML to BoogiePL, so that the BoogiePL verification condition generator can be used; and CCT, a tool to store proofs in class files.

AB - The Bytecode Modeling Language (BML) is a specification language for Java bytecode, that provides a high level of abstraction, while not restricting the format of the bytecode. Notably, BML specifications can be stored in class files, so that they can be shipped together with the bytecode. This makes BML particularly suited as property specification language in a proof-carrying code framework. Moreover, BML is designed to be close to the source code level specification language JML, so that specifications (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 specifications; Umbra, a BML viewer and editor, integrated in Eclipse; JML2BML, a compiler from JML to BML specifications; BMLt2BPL, a translator from BML to BoogiePL, so that the BoogiePL verification condition generator can be used; and CCT, a tool to store proofs in class files.

KW - METIS-263979

KW - IR-67853

KW - Program Verification

KW - tool support

KW - proof carrying code

KW - Specification

KW - Verification

KW - EWI-15929

KW - bytecode

U2 - 10.1007/978-3-642-04167-9_14

DO - 10.1007/978-3-642-04167-9_14

M3 - Conference contribution

SN - 978-3-642-04166-2

T3 - Lecture Notes in Computer Science

SP - 278

EP - 297

BT - Formal Methods for Components and Objects

A2 - de Boer, F.S

A2 - Bonsangue, M.M.

A2 - Madelaine, E.

PB - Springer

CY - London

Y2 - 21 October 2008 through 23 October 2008

ER -