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

    55 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