User menu

Static program analysis for Java Card applets

Bibliographic reference Almaliotis, V. ; Loizidis, A. ; Katsaros, P. ; Louridas, P. ; Spinellis, D.. Static program analysis for Java Card applets.Smart Card Research and Advanced Applications. 8th IFIP WG 8.8/11.2 International Conference, CARDIS 2008 (London, UK, 8-11 September 2008). In: Grimaud, G.; Standaert, F.-X.;, Smart Card Research and Advanced Applications. 8th IFIP WG 8.8/11.2 International Conference, CARDIS 2008, Springer-verlag2008, p. 17-31
Permanent URL
  1. Burdy, L., Requet, A., Lanet, J.L.: Java applet correctness: a developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, Springer, Heidelberg (2003)
  2. Beckert Bernhard, Mostowski Wojciech, A Program Logic for Handling Java Card’s Transaction Mechanism, Fundamental Approaches to Software Engineering (2003) ISBN:9783540008996 p.246-260, 10.1007/3-540-36578-8_18
  3. Marché C., Paulin-Mohring C., Urbain X., The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML, 10.1016/j.jlap.2003.07.006
  4. Meyer Jörg, Poetzsch-Heffter Arnd, An Architecture for Interactive Program Provers, Tools and Algorithms for the Construction and Analysis of Systems (2000) ISBN:9783540672821 p.63-77, 10.1007/3-540-46419-0_6
  5. Jacobs Bart, Marché Claude, Rauch Nicole, Formal Verification of a Commercial Smart Card Applet with Multiple Tools, Algebraic Methodology and Software Technology (2004) ISBN:9783540223818 p.241-257, 10.1007/978-3-540-27815-3_21
  6. van den Berg Joachim, Jacobs Bart, The loop Compiler for Java and JML, Tools and Algorithms for the Construction and Analysis of Systems (2001) ISBN:9783540418658 p.299-312, 10.1007/3-540-45319-9_21
  7. Breunesse C.-B., Cataño N., Huisman M., Jacobs B., Formal methods for smart cards: an experience report, 10.1016/j.scico.2004.05.011
  8. The Java Verifier project,
  9. Cataño Néstor, Huisman Marieke, Formal Specification and Static Checking of Gemplus’ Electronic Purse Using ESC/Java, FME 2002:Formal Methods—Getting IT Right (2002) ISBN:9783540439288 p.272-289, 10.1007/3-540-45614-7_16
  10. Meijer Hans, Poll Erik, Towards a Full Formal Specification of the JavaCard API, Smart Card Programming and Security (2001) ISBN:9783540426103 p.165-178, 10.1007/3-540-45418-7_14
  11. Spinellis Diomidis, Louridas Panagiotis, A framework for the static verification of api calls, 10.1016/j.jss.2006.09.040
  12. The FindBugs project (last access: Febuary 21, 2008),
  13. Hovemeyer David, Pugh William, Finding bugs is easy, 10.1145/1052883.1052895
  14. Dahm, M.: Byte code engineering with the BCEL API. Technical Report B-17-98, Freie University of Berlin, Institute of Informatics (2001)
  15. Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Proc. of the ACM SIGPLAN 2002 Conf. on Programming Language Design and Implementation (PLDI), pp. 57–68 (2002)
  16. Hampapuram Hari, Yang Yue, Das Manuvir, Symbolic path simulation in path-sensitive dataflow analysis, 10.1145/1108792.1108808
  17. Dhurjati Dinakar, Das Manuvir, Yang Yue, Path-Sensitive Dataflow Analysis with Iterative Refinement, Static Analysis (2006) ISBN:9783540377566 p.425-442, 10.1007/11823230_27
  18. The SAFE (Scalable And Flexible Error detection) project (last access: 21st of Febuary 2008) ,
  19. Strom Robert E., Yemini Shaula, Typestate: A programming language concept for enhancing software reliability, 10.1109/tse.1986.6312929
  20. Fink Stephen, Yahav Eran, Dor Nurit, Ramalingam G., Geay Emmanuel, Effective typestate verification in the presence of aliasing, 10.1145/1146238.1146254
  21. Chugunov, G., Fredlund, L.-A., Gurov, D.: Model checking of multi-applet Java Card Applications. In: Proc. of the 5th Smart Card Research and Advanced Application Conf. (CARDIS) (2002)