A. Amighi, S. C. Blom, M. Huisman, and M. Zaharieva-stojanovski, The VerCors project, Proceedings of the sixth workshop on Programming languages meets program verification, PLPV '12, pp.71-82, 2012.
DOI : 10.1145/2103776.2103785

B. Beckert, R. Hähnle, and P. H. Schmitt, Verification of Object-Oriented Software: The KeY Approach, volume 4334 of LNAI, 2007.

B. Beckert and W. Mostowski, A Program Logic for Handling Java Card???s Transaction Mechanism, Fundamental Approaches to Software Engineering, pp.246-260, 2003.
DOI : 10.1007/3-540-36578-8_18

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry et al., An overview of JML tools and applications, 8th Int'l Workshop on Formal Methods for Industrial Critical Systems, pp.73-89, 2003.
DOI : 10.1007/s10009-004-0167-4

L. Burdy, A. Requet, and J. Lanet, Java Applet Correctness: A Developer-Oriented Approach, International Symposium of Formal Methods Europe, pp.422-439, 2003.
DOI : 10.1007/978-3-540-45236-2_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.3304

Z. Chen, Java Card Technology for Smart Cards: Architecture and Programmer's Guide, 2000.

D. Distefano and M. J. Parkinson, jStar, ACM SIGPLAN Notices, vol.43, issue.10, pp.213-226, 2008.
DOI : 10.1145/1449955.1449782

D. Harel, D. Kozen, and J. Tiuryn, Dynamic Logic, 2000.

E. Hubbers and E. Poll, Reasoning about Card Tears and??Transactions??in??Java??Card, Fundamental Approaches to Software Engineering, pp.114-128, 2004.
DOI : 10.1007/978-3-540-24721-0_8

B. Jacobs, J. Smans, P. Philippaerts, and F. Piessens, The VeriFast program verifier ? a tutorial for Java Card developers, 2011.

B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx et al., VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, NASA Formal Methods, pp.41-55, 2011.
DOI : 10.1007/11691372_19

I. T. Kassios, Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions, LNCS, vol.4085, 2006.
DOI : 10.1007/11813040_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.166.61

J. Kwon and A. J. Wellings, Memory Management Based on Method Invocation in RTSJ, Proceedings, On the Move to Meaningful Internet Systems (OTM), pp.333-345, 2004.
DOI : 10.1007/978-3-540-30470-8_49

K. R. Leino, Dafny: An Automatic Program Verifier for Functional Correctness, LPAR (Dakar), pp.348-370, 2010.
DOI : 10.1007/978-3-642-17511-4_20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.9592

K. R. Leino, P. Müller, and J. Smans, Verification of Concurrent Programs with Chalice, Foundations of Security Analysis and Design, pp.195-222, 2009.
DOI : 10.1145/1375581.1375624

C. Marché, C. Paulin-mohring, and X. Urbain, The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML, The Journal of Logic and Algebraic Programming, vol.58, issue.1-2, pp.89-106, 2004.
DOI : 10.1016/j.jlap.2003.07.006

C. Marché and N. Rousset, Verification of JAVA CARD Applets Behavior with Respect to Transactions and Card Tears, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), 2006.
DOI : 10.1109/SEFM.2006.38

W. Mostowski, Formal Reasoning About Non-atomic Java Card Methods in Dynamic Logic, LNCS, vol.4085, pp.444-459, 2006.
DOI : 10.1007/11813040_30

W. Mostowski, Fully verified Java Card API reference implementation, 4th Int'l Verification Workshop, 2007.

W. Mostowski and E. Poll, Malicious Code on Java Card Smartcards: Attacks and Countermeasures, Smart Card Research and Advanced Application Conference, pp.1-16, 2008.
DOI : 10.1007/978-3-540-30569-9_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.123.6078

P. L. Pallec, A. Saif, O. Briot, M. Bensimon, J. Devisme et al., NFC cardlet development guidelines v2.2, 2012.

M. J. Parkinson and A. J. Summers, The relationship between separation logic and implicit dynamic frames, European Symposium on Programming, pp.439-458, 2011.

P. H. Schmitt, M. Ulbrich, and B. Weiß, Dynamic Frames in Java Dynamic Logic, Formal Verification of Object-Oriented Software Conference, pp.138-152, 2011.
DOI : 10.1007/978-3-540-27815-3_37

K. Stenzel, A Formally Verified Calculus for Full Java Card, Algebraic Methodology and Software Technology, 2004.
DOI : 10.1007/978-3-540-27815-3_37
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.147.2242