The Operational Semantics of a Java Secure Processor

Pieter H. Hartel, M.J. Butler, M. Levy

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

    36 Downloads (Pure)

    Abstract

    A formal specification of a Java Secure Processor is presented, which is mechanically checked for type consistency, well formedness and operational conservativity. The specification is executable and it is used to animate and study the behaviour of sample Java programs. The purpose of the semantics is to document the behaviour of the complete JSP for the benefit of implementors.
    Original languageUndefined
    Title of host publicationFormal Syntax and Semantics of Java
    EditorsJ. Alves-Foss
    Place of PublicationBerlin
    PublisherSpringer
    Pages313-352
    Number of pages40
    ISBN (Print)3-540-66158-1
    DOIs
    Publication statusPublished - 1999

    Publication series

    Name
    PublisherSpringer-Verlag

    Keywords

    • EWI-1037
    • IR-55694
    • SCS-Cybersecurity

    Cite this

    Hartel, P. H., Butler, M. J., & Levy, M. (1999). The Operational Semantics of a Java Secure Processor. In J. Alves-Foss (Ed.), Formal Syntax and Semantics of Java (pp. 313-352). Berlin: Springer. https://doi.org/10.1007/3-540-48737-9_9
    Hartel, Pieter H. ; Butler, M.J. ; Levy, M. / The Operational Semantics of a Java Secure Processor. Formal Syntax and Semantics of Java. editor / J. Alves-Foss. Berlin : Springer, 1999. pp. 313-352
    @inbook{626d8515d45f480092d50f703da4049d,
    title = "The Operational Semantics of a Java Secure Processor",
    abstract = "A formal specification of a Java Secure Processor is presented, which is mechanically checked for type consistency, well formedness and operational conservativity. The specification is executable and it is used to animate and study the behaviour of sample Java programs. The purpose of the semantics is to document the behaviour of the complete JSP for the benefit of implementors.",
    keywords = "EWI-1037, IR-55694, SCS-Cybersecurity",
    author = "Hartel, {Pieter H.} and M.J. Butler and M. Levy",
    note = "Imported from DIES",
    year = "1999",
    doi = "10.1007/3-540-48737-9_9",
    language = "Undefined",
    isbn = "3-540-66158-1",
    publisher = "Springer",
    pages = "313--352",
    editor = "J. Alves-Foss",
    booktitle = "Formal Syntax and Semantics of Java",

    }

    Hartel, PH, Butler, MJ & Levy, M 1999, The Operational Semantics of a Java Secure Processor. in J Alves-Foss (ed.), Formal Syntax and Semantics of Java. Springer, Berlin, pp. 313-352. https://doi.org/10.1007/3-540-48737-9_9

    The Operational Semantics of a Java Secure Processor. / Hartel, Pieter H.; Butler, M.J.; Levy, M.

    Formal Syntax and Semantics of Java. ed. / J. Alves-Foss. Berlin : Springer, 1999. p. 313-352.

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

    TY - CHAP

    T1 - The Operational Semantics of a Java Secure Processor

    AU - Hartel, Pieter H.

    AU - Butler, M.J.

    AU - Levy, M.

    N1 - Imported from DIES

    PY - 1999

    Y1 - 1999

    N2 - A formal specification of a Java Secure Processor is presented, which is mechanically checked for type consistency, well formedness and operational conservativity. The specification is executable and it is used to animate and study the behaviour of sample Java programs. The purpose of the semantics is to document the behaviour of the complete JSP for the benefit of implementors.

    AB - A formal specification of a Java Secure Processor is presented, which is mechanically checked for type consistency, well formedness and operational conservativity. The specification is executable and it is used to animate and study the behaviour of sample Java programs. The purpose of the semantics is to document the behaviour of the complete JSP for the benefit of implementors.

    KW - EWI-1037

    KW - IR-55694

    KW - SCS-Cybersecurity

    U2 - 10.1007/3-540-48737-9_9

    DO - 10.1007/3-540-48737-9_9

    M3 - Chapter

    SN - 3-540-66158-1

    SP - 313

    EP - 352

    BT - Formal Syntax and Semantics of Java

    A2 - Alves-Foss, J.

    PB - Springer

    CY - Berlin

    ER -

    Hartel PH, Butler MJ, Levy M. The Operational Semantics of a Java Secure Processor. In Alves-Foss J, editor, Formal Syntax and Semantics of Java. Berlin: Springer. 1999. p. 313-352 https://doi.org/10.1007/3-540-48737-9_9