@CONFERENCE\{IMM2005-04032,
    author       = "R. R. Hansen and I. Siveroni",
    title        = "Towards Verification of Well-Formed Transactions in Java Card Bytecode",
    year         = "2005",
    keywords     = "java card, static analysis, well-formed transactions, flow logic",
    booktitle    = "Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE)",
    volume       = "",
    series       = "Electronic Notes in Computer Science",
    editor       = "Fausto Spoto",
    publisher    = "Elsevier",
    organization = "",
    address      = "",
    note         = "To appear",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/4032-full.html",
    abstract     = "Using transactions in Java Card bytecode programs can be rather tricky
and requires special attention from the programmer in order to work
around some of the limitations imposed and to avoid introducing
serious run-time errors due to inappropriate use of transactions.

In this paper we present a novel analysis that combines control and
data flow analysis with an analysis that tracks active transactions in
a Java Card bytecode program. We formally prove the correctness of the
analysis and show how it can be used to solve the above problem of
guaranteeing that transactions in a Java Card bytecode program are
well-formed and thus do not give rise to run-time errors."
}