- We present a refinement method for Java programs which is motivated by the challenge of verifying security protocol implementations. The method can be used for stepwise refinement of abstract specifications down to the level of code running in the real application. The approach is based on a calculus for the verification of Java programs for the concrete level and Abstract State Machines for the abstract level. In this paper we illustrate our approach with the verification of a MCommerce application for buying movie tickets using a mobile phone written in J2ME. The approach uses the interactive theorem prover KIV.
