BML and Related Tools

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 languageUndefined
Title of host publicationFormal Methods for Components and Objects
EditorsF.S de Boer, M.M. Bonsangue, E. Madelaine
Place of PublicationLondon
PublisherSpringer
Pages278-297
Number of pages20
ISBN (Print)978-3-642-04166-2
DOIs
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume5751

Keywords

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

Cite this

Chrząszcz, J., Huisman, M., & Schubert, A. (2009). BML and Related Tools. In F. S. de Boer, M. M. Bonsangue, & E. Madelaine (Eds.), Formal Methods for Components and Objects (pp. 278-297). [10.1007/978-3-642-04167-9_14] (Lecture Notes in Computer Science; Vol. 5751). London: Springer. https://doi.org/10.1007/978-3-642-04167-9_14
Chrząszcz, J. ; Huisman, Marieke ; Schubert, A. / BML and Related Tools. Formal Methods for Components and Objects. editor / F.S de Boer ; M.M. Bonsangue ; E. Madelaine. London : Springer, 2009. pp. 278-297 (Lecture Notes in Computer Science).
@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ąszcz and Marieke Huisman and A. Schubert",
note = "Work done in the context of the IST-FET-2005-015905 Mobius project.",
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",

}

Chrząszcz, J, Huisman, M & Schubert, A 2009, BML and Related Tools. in FS de Boer, MM Bonsangue & E Madelaine (eds), Formal Methods for Components and Objects., 10.1007/978-3-642-04167-9_14, Lecture Notes in Computer Science, vol. 5751, Springer, London, pp. 278-297. https://doi.org/10.1007/978-3-642-04167-9_14

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 proceedingConference contributionAcademicpeer-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

ER -

Chrząszcz J, Huisman M, Schubert A. BML and Related Tools. In de Boer FS, Bonsangue MM, Madelaine E, editors, Formal Methods for Components and Objects. London: Springer. 2009. p. 278-297. 10.1007/978-3-642-04167-9_14. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-04167-9_14