JACK: Java Applet Correctness Kit

The paper presents a solution to improve the applet quality by allowing proof on Java Card TM annotated applets. It presents the chosen annotation language: JML that allows to formally specify each method and to give properties on fields. The innovative part of the paper is the presentation of the tools developed in the Gemplus Software Research Labs which allows proving the annotation by translating them in a formal language. To reduce the difficulty of using formal techniques, the tools aim to provide a user-friendly interface which hides to developers most of the formal features and provides him a "Java view" of proofs