BML and Related Tools

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    4 Citations (Scopus)
    23 Downloads (Pure)


    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
    Number of pages20
    ISBN (Print)978-3-642-04166-2
    Publication statusPublished - 2009
    EventFormal Methods for Components and Objects - Sophia Antipolis, France
    Duration: 21 Oct 200823 Oct 2008

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag


    ConferenceFormal Methods for Components and Objects
    Other21-23 Oktober 2008


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

    Cite this