Article ID Journal Published Year Pages File Type
10328860 Electronic Notes in Theoretical Computer Science 2005 18 Pages PDF
Abstract
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.
Keywords
Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Preview
Towards Verification of Well-Formed Transactions in Java Card Bytecode
Authors
, ,