Entry Stata:1999:TSJ from toplas.bib

Last update: Tue May 1 02:05:46 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Stata:1999:TSJ,
  author =       "Raymie Stata and Martin Abadi",
  title =        "A Type System for {Java} Bytecode Subroutines",
  journal =      j-TOPLAS,
  volume =       "21",
  number =       "1",
  pages =        "90--137",
  month =        jan,
  year =         "1999",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Tue Sep 26 10:12:58 MDT 2000",
  bibsource =    "http://www.acm.org/pubs/contents/journals/toplas/;
                 http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  URL =          "http://www.acm.org/pubs/citations/journals/toplas/1999-21-1/p90-stata/",
  abstract =     "Java is typically compiled into an intermediate
                 language, JVML, that is interpreted by the Java Virtual
                 Machine. Because mobile JVML code is not always
                 trusted, a bytecode verifier enforces static
                 constraints that prevent various dynamic errors. Given
                 the importance of the bytecode verifier for security,
                 its current descriptions are inadequate. This article
                 proposes using typing rules to describe the bytecode
                 verifier because they are more precise than prose,
                 clearer than code, and easier to reason about than
                 either. JVML has a subroutine construct which is used
                 for the compilation of Java's try-finally statement.
                 Subroutines are a major source of complexity for the
                 bytecode verifier because they are not obviously
                 last-in/first-out and because they require a kind of
                 polymorphism. Focusing on subroutines, we isolate an
                 interesting, small subset of JVML. We give typing rules
                 for this subset and prove their correctness. Our type
                 system constitutes a sound basis for bytecode
                 verification and a rational reconstruction of a
                 delicate part of Sun's bytecode verifier.",
  acknowledgement = ack-nhfb,
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  keywords =     "bytecode verification; Java; languages; security;
                 theory; verification",
  subject =      "Software --- Programming Languages --- Language
                 Classifications (D.3.2): {\bf Java}; Software ---
                 Programming Languages --- Formal Definitions and Theory
                 (D.3.1): {\bf Semantics}; Software --- Operating
                 Systems --- Security and Protection (D.4.6): {\bf
                 Invasive software}; Theory of Computation --- Logics
                 and Meanings of Programs --- Semantics of Programming
                 Languages (F.3.2): {\bf Operational semantics}; Theory
                 of Computation --- Logics and Meanings of Programs ---
                 Semantics of Programming Languages (F.3.2): {\bf
                 Program analysis}; Theory of Computation --- Logics and
                 Meanings of Programs --- Studies of Program Constructs
                 (F.3.3): {\bf Type structure}",
}

Related entries