The paper describes an experiment in which a framework for model checking Java byte code, combined with the application of runtime monitoring techniques through code rewriting, was used to guarantee correctness properties of a Java Card applet.
In: Proceedings of the RV'04 workshop (Runtime Verification '04), at Barcelona