Guaranteeing Correctness Properties of a Java Card Applet

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.